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.
• nextBoundary: the next interval start above a, or the upper endpoint N.

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

Every interval start chart.start j is strictly below 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

A word x inside interval j is reached from chart.start j after x.toNat - chart.start j steps of f.

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.

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_le_of_mem (S : Finset ℕ) (N a b : ℕ) (hb : b ∈ S) (hab : a < b) : nextBoundary S N a ≤ b

Every element b ∈ S strictly above a is an upper bound on nextBoundary S N a.

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.