Canonical cycle labels as bit strings

Order n-bit states lexicographically, coordinate zero first (lexOrder). The canonical label of a state x under f lists the least state of its eventual cycle, the cycle length and the phase of x on the cycle, the last two in n + 3 bits (canonicalLabel). Labels along an orbit differ only in the phase, so the label of x is recovered from the label of f^[j] x by subtracting j modulo the cycle length (correctLabel_canonicalLabel).

On a cycle of length at most K, the first K + 1 states of the orbit of a periodic state contain the whole cycle. A scan for the least of them, the first return to x and the first visit to the least state give its label directly (shortLabel_eq_canonicalLabel), in O(K * n + n ^ 2) gates once the orbit prefix is available (synthesis_shortLabel).

Main definitions

• Cslib.Circuits.Boolean.Iteration.canonicalLabel: representative, cycle length and phase.
• Cslib.Circuits.Boolean.Iteration.correctLabel: shift a label back along the orbit.
• Cslib.Circuits.Boolean.Iteration.shortLabel: the label read from one traversal of a short cycle.

Main results

• Cslib.Circuits.Boolean.Iteration.correctLabel_canonicalLabel: correcting a later label.
• Cslib.Circuits.Boolean.Iteration.shortLabel_eq_canonicalLabel: short cycles.
• Cslib.Circuits.Boolean.Iteration.synthesis_correctLabel, Cslib.Circuits.Boolean.Iteration.synthesis_shortLabel: their gate counts.

References

• Adapted from lean/Proofs/{ShortCycle,LabelEncoding}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Label words

def Cslib.Circuits.Boolean.Iteration.labelBits {n w : ℕ} (c : BitString n) (ell phi : BitVec w) : BitString (n + (w + w))

A state followed by two words.

def Cslib.Circuits.Boolean.Iteration.labelRepresentative {n w : ℕ} (r : BitString (n + (w + w))) : BitString n

The state of a label.

def Cslib.Circuits.Boolean.Iteration.labelLength {n w : ℕ} (r : BitString (n + (w + w))) : BitVec w

The first word of a label: the cycle length.

def Cslib.Circuits.Boolean.Iteration.labelPhase {n w : ℕ} (r : BitString (n + (w + w))) : BitVec w

The second word of a label: the phase.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.labelRepresentative_labelBits {n w : ℕ} (c : BitString n) (ell phi : BitVec w) : labelRepresentative (labelBits c ell phi) = c

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.labelLength_labelBits {n w : ℕ} (c : BitString n) (ell phi : BitVec w) : labelLength (labelBits c ell phi) = ell

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.labelPhase_labelBits {n w : ℕ} (c : BitString n) (ell phi : BitVec w) : labelPhase (labelBits c ell phi) = phi

@[reducible, inline]

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

The width of a canonical label: a state, then two words of n + 3 bits.

noncomputable def Cslib.Circuits.Boolean.Iteration.canonicalLabel {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : BitString (labelWidth n)

Canonical labels. The lexicographically least state of the eventual cycle of x, the cycle length, and the phase of x on the cycle, the last two in n + 3 bits.

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

theorem Cslib.Circuits.Boolean.Iteration.toNat_ofNat_cycleLength {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : (BitVec.ofNat (n + 3) (FunctionalGraph.cycleLength f x)).toNat = FunctionalGraph.cycleLength f x

theorem Cslib.Circuits.Boolean.Iteration.toNat_ofNat_phase {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : (BitVec.ofNat (n + 3) (FunctionalGraph.phase f x)).toNat = FunctionalGraph.phase f x

Correcting labels along an orbit

def Cslib.Circuits.Boolean.Iteration.correctLabel {n w : ℕ} (r : BitString (n + (w + w))) (j : ℕ) : BitString (n + (w + w))

Shift a label back by j steps: subtract j from its phase modulo its cycle length.

theorem Cslib.Circuits.Boolean.Iteration.correctLabel_canonicalLabel {n : ℕ} (f : BitString n → BitString n) (x : BitString n) (j : ℕ) (hj : j < 2 ^ (n + 3)) : correctLabel (canonicalLabel f (f^[j] x)) j = canonicalLabel f x

The label of x is the label of f^[j] x shifted back by j, for j < 2 ^ (n + 3).

theorem Cslib.Circuits.Boolean.Iteration.labelBits_wires_subset {n a w : ℕ} (s : Set (BooleanFunction a)) (c : BitString a → BitString n) (ell phi : BitString a → BitVec w) (hc : wires c ⊆ s) (he : wordWires ell ⊆ s) (hp : wordWires phi ⊆ s) : (wires fun (x : BitString a) => labelBits (c x) (ell x) (phi x)) ⊆ s

The bits of a label of available parts are available.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_correctLabel {n a w : ℕ} (s : Set (BooleanFunction a)) (r : BitString a → BitString (n + (w + w))) (hr : wires r ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) (j : ℕ) : Synthesis interpretation s (wires fun (x : BitString a) => correctLabel (r x) j) (50 * (w + 1) ^ 2)

Correcting an available label costs one modular difference.

Short cycles

noncomputable def Cslib.Circuits.Boolean.Iteration.shortRepresentative {n : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) : BitString n

The least of the first K + 1 states of the orbit of x.

def Cslib.Circuits.Boolean.Iteration.shortLength {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) : BitVec w

The first positive time up to K at which the orbit of x returns to x.

noncomputable def Cslib.Circuits.Boolean.Iteration.shortTime {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) : BitVec w

The first time up to K at which the orbit of x visits its short representative.

noncomputable def Cslib.Circuits.Boolean.Iteration.shortLabel {n : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) : BitString (labelWidth n)

The label read from the first K + 1 states of the orbit of x.

theorem Cslib.Circuits.Boolean.Iteration.shortRepresentative_eq {n : ℕ} (f : BitString n → BitString n) (K : ℕ) {x : BitString n} (hx : x ∈ Function.periodicPts f) (hK : FunctionalGraph.cycleLength f x ≤ K) : shortRepresentative f K x = FunctionalGraph.canonicalCycle f x

theorem Cslib.Circuits.Boolean.Iteration.shortLength_eq {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) {x : BitString n} (hx : x ∈ Function.periodicPts f) (hK : FunctionalGraph.cycleLength f x ≤ K) : shortLength f K x = BitVec.ofNat w (FunctionalGraph.cycleLength f x)

theorem Cslib.Circuits.Boolean.Iteration.shortTime_eq {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) {x : BitString n} (hx : x ∈ Function.periodicPts f) (hK : FunctionalGraph.cycleLength f x ≤ K) : shortTime f K x = BitVec.ofNat w (FunctionalGraph.canonicalTime f x)

theorem Cslib.Circuits.Boolean.Iteration.shortLabel_eq_canonicalLabel {n : ℕ} (f : BitString n → BitString n) (K : ℕ) {x : BitString n} (hx : x ∈ Function.periodicPts f) (hK : FunctionalGraph.cycleLength f x ≤ K) : shortLabel f K x = canonicalLabel f x

Short cycles. On a periodic state whose cycle has length at most K, the label read from the first K + 1 states of its orbit is its canonical label.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_shortLabel {n a : ℕ} (s : Set (BooleanFunction a)) (f : BitString n → BitString n) (init : BitString a → BitString n) (K : ℕ) (hp : ∀ (j : Fin (K + 1)) (bit : Fin n), (fun (x : BitString a) => f^[↑j] (init x) bit) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wires fun (x : BitString a) => shortLabel f K (init x)) ((K + 1) * (30 * n + 27) + 50 * (n + 4) ^ 2)

Short-cycle labels. Once the first K + 1 states of an orbit are available, its short label costs one minimum scan, two first-position scans, their equality tests and one modular difference.