Sparse orbit coordinates from interval labels

Each interval stores its cycle representative, cycle length, and the phase of its first state. One modular addition encodes its other states. Decoding tests the phase distance from each interval start. This proves a chart without an enumeration of payload states or an assumed constant-time table primitive.

Main definitions

• chartWidth: widened bit-vector width n + 2 for cycle lengths and phases.
• wordCycleLabel: canonical word-cycle coordinates.
• CounterIntervalChart.first, CounterIntervalChart.period, CounterIntervalChart.initialPhase, CounterIntervalChart.length, CounterIntervalChart.contains, CounterIntervalChart.offset, CounterIntervalChart.encodedRow: per-interval parameters, membership test, offset, and predicted coordinates.
• CounterIntervalChart.encode: select the coordinates of a containing interval.

Main results

• CounterIntervalChart.encode_spec: the selected coordinates are canonical.

References

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

@[instance_reducible]

def Cslib.Circuits.Boolean.Iteration.counterChartWordOrder (n : ℕ) : LinearOrder (BitVec n)

Numeric order chooses canonical representatives of word cycles. Kept local to charts.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Iteration.chartWidth (n : ℕ) : ℕ

Two spare bits hold cycle lengths and sums even for a cycle of length 2^n.

theorem Cslib.Circuits.Boolean.Iteration.cycleLength_le_words {n : ℕ} (f : BitVec n → BitVec n) (x : BitVec n) : FunctionalGraph.cycleLength f x ≤ 2 ^ n

Every cycle length of a map on BitVec n is at most 2 ^ n.

theorem Cslib.Circuits.Boolean.Iteration.chart_ofNat_toNat {n a : ℕ} (ha : a ≤ 2 ^ n) : (BitVec.ofNat (chartWidth n) a).toNat = a

Any natural number a ≤ 2 ^ n fits without wraparound in BitVec (chartWidth n).

noncomputable def Cslib.Circuits.Boolean.Iteration.wordCycleLabel {n : ℕ} (f : BitVec n → BitVec n) (x : BitVec n) : BitString (n + (chartWidth n + chartWidth n))

Canonical coordinates of a cyclic word.

def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.first {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : BitVec n

The first word of an interval.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.period {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : BitVec (chartWidth n)

Cycle length of the interval, in the widened coordinate width.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.initialPhase {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : BitVec (chartWidth n)

Canonical phase of the interval start.

def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.length {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : BitVec (chartWidth n)

Number of words in an interval.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.period_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : (chart.period j).toNat = FunctionalGraph.cycleLength f (chart.first j)

The natural-number value of chart.period j is the cycle length of chart.first j.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.initialPhase_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : (chart.initialPhase j).toNat = FunctionalGraph.phase f (chart.first j)

The natural-number value of chart.initialPhase j is the phase of chart.first j.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.length_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : (chart.length j).toNat = chart.stop j - chart.start j

The natural-number value of chart.length j is chart.stop j - chart.start j.

def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.contains {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) : Bool

Test membership in the half-open numerical interval.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.contains_iff {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) : chart.contains j x = true ↔ chart.start j ≤ x.toNat ∧ x.toNat < chart.stop j

chart.contains j x is true iff x.toNat lies in [chart.start j, chart.stop j).

def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.offset {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) : BitVec (chartWidth n)

Numerical distance from the interval start.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.encodedRow {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) : BitString (n + (chartWidth n + chartWidth n))

Canonical coordinates predicted by one interval.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.encode {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (x : BitVec n) : BitString (n + (chartWidth n + chartWidth n))

Encode by selecting any interval containing the input.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.encode_spec {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (x : BitVec n) : chart.encode x = wordCycleLabel f x

Encoding a word x under an injective map f produces its canonical cycle coordinates wordCycleLabel f x.