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

• wordCycleLabel: canonical word-cycle 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

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

theorem Cslib.Circuits.Boolean.Iteration.chart_setWidth_toNat {n : ℕ} (x : BitVec n) : (BitVec.setWidth (chartWidth n) x).toNat = x.toNat

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)

@[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)

@[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

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

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.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.offset_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (x : BitVec n) (hx : chart.start j ≤ x.toNat) : (chart.offset j x).toNat = x.toNat - chart.start j

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.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.encodedRow_spec {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) (x : BitVec n) (hx : chart.contains j x = true) : chart.encodedRow j x = wordCycleLabel f x

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