Circuits for canonical cycle labels

Let c be a circuit of size s computing f on n-bit states. Some circuit of size at most 60000 * powerBudget n s (2 ^ n) L computes the canonical label of every state: the lexicographically least state of its eventual cycle, the cycle length and its phase (cycle_label_circuit), for every 0 < L ≤ 2 ^ n; with the balanced parameter the size is at most 180000 * optimizedBudget n s (2 ^ n) (cycle_labels_optimized).

The construction first applies f^[(2 ^ n)!] with a fixed-power circuit. This moves every state onto its cycle without changing its label. On a periodic state, choose checkpoints as for fixed powers and hardwire the label of each. The first 2 L + 1 states of the orbit are looked up in one shared dictionary (lookupOr); a checkpoint hit at time j gives the label after shifting its phase back by j (correctLabel_canonicalLabel). Without a hit the orbit repeats within L steps, so its cycle is short and is read off the orbit prefix (shortLabel_eq_canonicalLabel).

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. The checkpoints and their labels are chosen nonconstructively, so the circuits exist for each L; nothing here bounds the time to construct them.

Main definitions

• Cslib.Circuits.Boolean.Iteration.labelCost: the gate count of the checkpoint construction.

Main results

• Cslib.Circuits.Boolean.Iteration.cyclic_labels_from_checkpoints: labels of periodic states from given checkpoints.
• Cslib.Circuits.Boolean.Iteration.cyclic_label_circuit: labels of periodic states.
• Cslib.Circuits.Boolean.Iteration.cycle_label_circuit, Cslib.Circuits.Boolean.Iteration.cycle_labels_optimized: labels of all states.

References

• Adapted from lean/Proofs/LabelCircuits.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, whose bounds have the constants 10040000 and 30120000. The dictionary here is the library's batchOrCircuit lookup.

def Cslib.Circuits.Boolean.Iteration.labelCost (n s M L : ℕ) : ℕ

The gate count of the label construction from M checkpoints with parameter L: constants, the orbit prefix, the shared dictionary, one label correction per prefix state, the short-cycle label and the final selection.

theorem Cslib.Circuits.Boolean.Iteration.cyclic_labels_from_checkpoints {n M : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (cp : Fin M → BitString n) (hcp : Function.Injective cp) (hcover : ∀ (x : Fin n → Bool), FunctionalGraph.Repeats (c.eval interpretation) x L ∨ ∃ t < 2 * L, ∃ (j : Fin M), (c.eval interpretation)^[t] x = cp j) : ∃ (out : Circuit signature n (labelWidth n)), (∀ x ∈ Function.periodicPts (c.eval interpretation), out.eval interpretation x = canonicalLabel (c.eval interpretation) x) ∧ out.size ≤ labelCost n c.size M L

Labels from checkpoints. Let cp be injective checkpoints such that every orbit repeats among its first L states or reaches a checkpoint in fewer than 2 L steps. Then some circuit of size at most labelCost n c.size M L computes the canonical label of every periodic state.

theorem Cslib.Circuits.Boolean.Iteration.labelCost_le (n s M L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hM : M ≤ 2 ^ n / L) : labelCost n s M L ≤ 20000 * powerBudget n s (2 ^ n) L

The label construction is within 20000 times the fixed-power tradeoff.

theorem Cslib.Circuits.Boolean.Iteration.cyclic_label_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (labelWidth n)), (∀ x ∈ Function.periodicPts (c.eval interpretation), out.eval interpretation x = canonicalLabel (c.eval interpretation) x) ∧ out.size ≤ 20000 * powerBudget n c.size (2 ^ n) L

Labels of periodic states. For every 0 < L ≤ 2 ^ n, some circuit of size at most 20000 * powerBudget n c.size (2 ^ n) L computes the canonical label of every periodic state.

theorem Cslib.Circuits.Boolean.Iteration.canonicalLabel_iterate_factorial {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : canonicalLabel f (f^[(2 ^ n).factorial] x) = canonicalLabel f x

Moving a state onto its cycle with f^[(2 ^ n)!] does not change its label.

theorem Cslib.Circuits.Boolean.Iteration.iterate_factorial_mem_periodicPts {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : f^[(2 ^ n).factorial] x ∈ Function.periodicPts f

theorem Cslib.Circuits.Boolean.Iteration.cycle_label_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (labelWidth n)), out.Computes interpretation (canonicalLabel (c.eval interpretation)) ∧ out.size ≤ 60000 * powerBudget n c.size (2 ^ n) L

Cycle labels. For every 0 < L ≤ 2 ^ n, some circuit of size at most 60000 * powerBudget n c.size (2 ^ n) L computes the canonical label of every state: the lexicographically least state of its eventual cycle, the cycle length and its phase.

theorem Cslib.Circuits.Boolean.Iteration.cycle_labels_optimized {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature n (labelWidth n)), out.Computes interpretation (canonicalLabel (c.eval interpretation)) ∧ ↑out.size ≤ 180000 * optimizedBudget n c.size (2 ^ n)

Square-root cycle labels. Some circuit of size at most 180000 * optimizedBudget n c.size (2 ^ n) computes the canonical label of every state.