Linear intervals between edited counter edges

Cut the ordinary linear order after each edited successor, and also at its two endpoints. There are at most r+1 intervals. Inside each interval the trajectory is ordinary increment, without circular wraparound. This is the semantic chart used by the sparse live-time circuit.

Main definitions

• CounterIntervalChart: intervals on which iteration is numerical translation.

Main results

• exists_counterIntervalChart: a cover with at most one more interval than edited edges.

References

• Adapted from lean/Proofs/CounterIntervals.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

structure Cslib.Circuits.Boolean.Iteration.CounterIntervalChart {n : ℕ} (f : BitVec n → BitVec n) (R : ℕ) : Type

A covering by ordinary intervals on which iteration is translation. No permutation hypothesis is needed for this local trajectory certificate.

• start : Fin R → ℕ

  First natural-number index of each interval.

• stop : Fin R → ℕ

  Exclusive upper endpoint of each interval.

• start_lt_stop (j : Fin R) : self.start j < self.stop j

  Each interval is nonempty.

• stop_le (j : Fin R) : self.stop j ≤ 2 ^ n

  Every interval stays within the word universe.

• covers (x : BitVec n) : ∃ (j : Fin R), self.start j ≤ x.toNat ∧ x.toNat < self.stop j

  Every word belongs to at least one interval.

• path (j : Fin R) (d : ℕ) : d < self.stop j - self.start j → f^[d] (BitVec.ofNat n (self.start j)) = BitVec.ofNat n (self.start j + d)

  Inside an interval, iteration agrees with numerical increment.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.start_lt {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : chart.start j < 2 ^ n

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.point_eq {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) (hlo : chart.start j ≤ x.toNat) (hhi : x.toNat < chart.stop j) : f^[x.toNat - chart.start j] (BitVec.ofNat n (chart.start j)) = x

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.length_le_period {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) : chart.stop j - chart.start j ≤ FunctionalGraph.cycleLength f (BitVec.ofNat n (chart.start j))

A nonrepeating interval cannot be longer than its permutation cycle.

noncomputable def Cslib.Circuits.Boolean.Iteration.counterIntervalStarts {n : ℕ} (f : BitVec n → BitVec n) : Finset ℕ

Starts of the linear pieces; the last counter edge creates no additional piece.

theorem Cslib.Circuits.Boolean.Iteration.counterIntervalStarts_bound {n : ℕ} (f : BitVec n → BitVec n) : (counterIntervalStarts f).card ≤ (FunctionalGraph.disagreement f fun (x : BitVec n) => x + 1).card + 1

theorem Cslib.Circuits.Boolean.Iteration.counterIntervalStarts_lt {n : ℕ} (f : BitVec n → BitVec n) {a : ℕ} (ha : a ∈ counterIntervalStarts f) : a < 2 ^ n

def Cslib.Circuits.Boolean.Iteration.nextBoundary (S : Finset ℕ) (N a : ℕ) : ℕ

The next start, or the upper endpoint of the whole universe.

theorem Cslib.Circuits.Boolean.Iteration.nextBoundary_gt (S : Finset ℕ) {N a : ℕ} (ha : a < N) : a < nextBoundary S N a

theorem Cslib.Circuits.Boolean.Iteration.nextBoundary_le (S : Finset ℕ) (N a : ℕ) : nextBoundary S N a ≤ N

theorem Cslib.Circuits.Boolean.Iteration.nextBoundary_le_of_mem (S : Finset ℕ) (N a b : ℕ) (hb : b ∈ S) (hab : a < b) : nextBoundary S N a ≤ b

theorem Cslib.Circuits.Boolean.Iteration.exists_covering_interval (S : Finset ℕ) {N x : ℕ} (hzero : 0 ∈ S) (hx : x < N) : ∃ a ∈ S, a ≤ x ∧ x < nextBoundary S N a

A finite set of starts containing zero covers the whole linear universe.

theorem Cslib.Circuits.Boolean.Iteration.counterInterval_step {n : ℕ} (f : BitVec n → BitVec n) {a i : ℕ} (hai : a ≤ i) (hi : i + 1 < nextBoundary (counterIntervalStarts f) (2 ^ n) a) : f (BitVec.ofNat n i) = BitVec.ofNat n (i + 1)

Before the next cut, the actual update agrees with numerical increment.

theorem Cslib.Circuits.Boolean.Iteration.exists_counterIntervalChart {n : ℕ} (f : BitVec n → BitVec n) : ∃ R ≤ (FunctionalGraph.disagreement f fun (x : BitVec n) => x + 1).card + 1, Nonempty (CounterIntervalChart f R)

Every sparse counter modification has a chart of at most r+1 intervals. This existence theorem does not charge a preprocessing algorithm.