Circuits for maps commuting with sparse counter modifications

If an injective word map h commutes with a map f differing from the binary counter at r inputs, then h has a native De Morgan circuit of at most 100 * (n + 1) * (r + 1) gates. The displacement h x - x changes at at most 2 * r counter edges. A telescoping sum of threshold corrections reconstructs it; comparisons, selectors, additions and constants are all charged. In particular the bound holds for every signed fixed power of a permutation.

These are nonuniform existence results. The correction table is chosen from the whole map; no efficient table-construction algorithm is asserted. A change of coordinates additionally requires circuits for both directions, whose sizes are charged explicitly.

Main definitions

• Cslib.Circuits.Boolean.Iteration.thresholdSum: a sum of corrections at passed thresholds.
• Cslib.Circuits.Boolean.Iteration.displacement, displacementCuts: displacement and its changes.

Main results

• Cslib.Circuits.Boolean.Iteration.thresholdSum_displacement: exact telescoping reconstruction.
• Cslib.Circuits.Boolean.Iteration.sparse_counter_centralizer: the sparse-counter circuit bound.
• Cslib.Circuits.Boolean.Iteration.sparse_counter_power: the bound for every integer power.
• Cslib.Circuits.Boolean.Iteration.sparse_coordinate_power: transfer through charged coordinates.

References

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

def Cslib.Circuits.Boolean.Iteration.thresholdSum {w : ℕ} (S : Finset ℕ) (coeff : ℕ → BitVec w) (base x : BitVec w) : BitVec w

Add the corrections whose thresholds precede the input word.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_thresholdSum {n w : ℕ} (S : Finset ℕ) (coeff : ℕ → BitVec w) (base : BitVec w) (s : Set (BitString n → Bool)) (a : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => thresholdSum S coeff base (a x)) (S.card * (21 * w + 3))

Each threshold uses one comparison, one word selector, and one shared-carry addition.

def Cslib.Circuits.Boolean.Iteration.displacement {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) : BitVec n

Word displacement relative to the counter coordinates.

def Cslib.Circuits.Boolean.Iteration.displacementCuts {n : ℕ} (h : BitVec n → BitVec n) : Finset ℕ

Changes of displacement, including the wraparound edge.

theorem Cslib.Circuits.Boolean.Iteration.displacement_change_iff {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) : displacement h (x + 1) ≠ displacement h x ↔ h (x + 1) ≠ h x + 1

theorem Cslib.Circuits.Boolean.Iteration.thresholdSum_displacement {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) : thresholdSum (displacementCuts h) (fun (i : ℕ) => displacement h (BitVec.ofNat n (i + 1)) - displacement h (BitVec.ofNat n i)) (displacement h 0) x = displacement h x

The sparse derivative reconstructs the entire word function by telescoping.

theorem Cslib.Circuits.Boolean.Iteration.displacementCuts_card {n : ℕ} (f h : BitVec n → BitVec n) (hc : Function.Commute h f) (hi : Function.Injective h) : (displacementCuts h).card ≤ 2 * (FunctionalGraph.disagreement f fun (x : BitVec n) => x + 1).card

Counter-coordinate changes inject into the commutation-defect set.

theorem Cslib.Circuits.Boolean.Iteration.displacement_circuit {n : ℕ} (h : BitVec n → BitVec n) : ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (h (word x)).getLsbD ↑i) ∧ out.size ≤ 2 + (displacementCuts h).card * (21 * n + 3) + (12 * n + 1)

A sparse derivative gives an actual native Boolean circuit, including all selection gates.

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_centralizer {n : ℕ} (f h : BitVec n → BitVec n) (hc : Function.Commute h f) (hi : Function.Injective h) : ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (h (word x)).getLsbD ↑i) ∧ out.size ≤ 100 * (n + 1) * ((FunctionalGraph.disagreement f fun (x : BitVec n) => x + 1).card + 1)

Every injective map commuting with an r-edited counter has size O(n(r+1)). No transition circuit or state-space enumeration is a hypothesis.

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_power {n : ℕ} (f : Equiv.Perm (BitVec n)) (T : ℤ) : ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((f ^ T) (word x)).getLsbD ↑i) ∧ out.size ≤ 100 * (n + 1) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + 1)

The bound applies uniformly to all signed fixed powers of a permutation.

theorem Cslib.Circuits.Boolean.Iteration.sparse_coordinate_power {n : ℕ} (f g e : Equiv.Perm (BitVec n)) (hcycle : ∀ (x : BitVec n), e (g x) = e x + 1) (encode decode : Circuit signature n n) (he : encode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (e (word x)).getLsbD ↑i) (hd : decode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((Equiv.symm e) (word x)).getLsbD ↑i) (T : ℤ) : ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((f ^ T) (word x)).getLsbD ↑i) ∧ out.size ≤ encode.size + decode.size + 100 * (n + 1) * ((FunctionalGraph.disagreement ⇑f ⇑g).card + 1)

Cheap orbit coordinates transfer the sparse bound, charging both conversion circuits.