Simulation, hardwiring, and a universal step map

If τ steps of U simulate one step of F on encoded states, then τ * T steps of U simulate T steps of F (iterate_simulation). When the encoding places the input bits among constant bits, a circuit for the power of U yields one for the power of F with at most two more gates, the two constants of the De Morgan basis (simulation_circuit).

The universal step map executes a straight-line program, held in its state, one gate per step, and after the last gate copies the output wires back into the input registers (Universal.step). One round of G + 1 steps runs any circuit with at most G gates (Universal.step_round): each gate evaluation and the simultaneous output copy/reset each count as one semantic step. Because Universal.Description and Universal.Config carry natural-number wire indices and a natural-number program counter (pc : ℕ), Universal.Config is an unbounded mathematical configuration space rather than a finite Boolean state space or the native certified universal Turing machine; the generic value carrier V uses [Inhabited V] as the default for out-of-range wire reads and cleared work registers. The circuit reduction Universal.universal_power_circuit is conditional: it assumes a finite bit encoding e, the start-state hardwiring equation he, and a circuit u computing (Universal.step interpretation)^[(G + 1) * T] on start states, without constructing a global finite state encoding or a circuit for one universal step. A group action by a hardwired element (smul_zpow_circuit, smul_iterate_circuit, smul_inverse_circuit), and either factor of a product map (prodMap_power_circuit, prodMap_power_circuit_left), are handled by the same hardwiring argument.

Main definitions

• Cslib.Circuits.Boolean.Iteration.hardwired: place input bits and constants on m wires.
• Cslib.Circuits.Boolean.Iteration.prodMap: product of two maps on concatenated bit strings.
• Cslib.Circuits.Boolean.Iteration.Universal.Description: straight-line program description held in the state of the universal step map.
• Cslib.Circuits.Boolean.Iteration.Universal.Config: configuration of the universal step map.
• Cslib.Circuits.Boolean.Iteration.Universal.step: one step of the universal step map.

Main results

• Cslib.Circuits.Boolean.Iteration.simulation_circuit: C(F^[T]) ≤ C(U^[τ * T]) + 2 under a hardwired simulation.
• Cslib.Circuits.Boolean.Iteration.prodMap_power_circuit, Cslib.Circuits.Boolean.Iteration.prodMap_power_circuit_left: factor reductions for product maps.
• Cslib.Circuits.Boolean.Iteration.smul_zpow_circuit, Cslib.Circuits.Boolean.Iteration.smul_iterate_circuit, Cslib.Circuits.Boolean.Iteration.smul_inverse_circuit: integer powers, iterates, and inverses of a group action by a fixed element.
• Cslib.Circuits.Boolean.Iteration.Universal.step_round, Cslib.Circuits.Boolean.Iteration.Universal.step_iterate, Cslib.Circuits.Boolean.Iteration.Universal.universal_power_circuit: simulation of any circuit of at most G gates by G + 1 steps of the universal map.

References

• Adapted from lean/Proofs/UniversalMap.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Simulation of powers

theorem Cslib.Circuits.Boolean.Iteration.iterate_simulation {α : Type u_1} {β : Type u_2} (enc : α → β) (F : α → α) (U : β → β) (τ : ℕ) (h : ∀ (x : α), U^[τ] (enc x) = enc (F x)) (T : ℕ) (x : α) : U^[τ * T] (enc x) = enc (F^[T] x)

One step of F is τ steps of U on encoded states, hence T steps are τ * T.

Hardwiring constants

def Cslib.Circuits.Boolean.Iteration.hardwired {n m : ℕ} (place : Fin m → Fin n ⊕ Bool) (x : BitString n) : BitString m

Place input bits and constants on m wires.

theorem Cslib.Circuits.Boolean.Iteration.exists_hardwired_comp {n m p : ℕ} (u : Circuit signature m p) (place : Fin m → Fin n ⊕ Bool) : ∃ (d : Circuit signature n p), (∀ (x : Fin n → Bool), d.eval interpretation x = u.eval interpretation (hardwired place x)) ∧ d.size ≤ u.size + 2

Hardwiring constants and duplicating or permuting inputs costs the two constants.

theorem Cslib.Circuits.Boolean.Iteration.exists_hardwired_projection {n m p k : ℕ} (u : Circuit signature m p) (place : Fin m → Fin n ⊕ Bool) (select : Fin k → Fin p) : ∃ (d : Circuit signature n k), (∀ (x : Fin n → Bool), d.eval interpretation x = u.eval interpretation (hardwired place x) ∘ select) ∧ d.size ≤ u.size + 2

Hardwire constants, run u, and read selected output wires.

theorem Cslib.Circuits.Boolean.Iteration.simulation_circuit {n m : ℕ} (F : BitString n → BitString n) (U : BitString m → BitString m) (place : Fin m → Fin n ⊕ Bool) (select : Fin n → Fin m) (hsel : ∀ (i : Fin n), place (select i) = Sum.inl i) (τ : ℕ) (hsim : ∀ (x : BitString n), U^[τ] (hardwired place x) = hardwired place (F x)) (T : ℕ) (u : Circuit signature m m) (hu : ∀ (x : BitString n), u.eval interpretation (hardwired place x) = U^[τ * T] (hardwired place x)) : ∃ (d : Circuit signature n n), d.Computes interpretation F^[T] ∧ d.size ≤ u.size + 2

The circuit consequence of a simulation: C(F^[T]) ≤ C(U^[τ * T]) + 2 when the encoding places the input bits among constants. The circuit for the power of U need only be correct on encoded states.

Products

def Cslib.Circuits.Boolean.Iteration.prodMap {m k : ℕ} (U : BitString m → BitString m) (P : BitString k → BitString k) (z : BitString (m + k)) : BitString (m + k)

The product of two maps on concatenated bit strings.

theorem Cslib.Circuits.Boolean.Iteration.prodMap_power_circuit {m k : ℕ} (U : BitString m → BitString m) (P : BitString k → BitString k) (T : ℕ) (u : Circuit signature (m + k) (m + k)) (hu : u.Computes interpretation (prodMap U P)^[T]) : ∃ (d : Circuit signature k k), d.Computes interpretation P^[T] ∧ d.size ≤ u.size + 2

Each power of a product map is at least as hard as the same power of its second factor: fix the first factor's input and read the second factor's outputs.

theorem Cslib.Circuits.Boolean.Iteration.prodMap_power_circuit_left {m k : ℕ} (U : BitString m → BitString m) (P : BitString k → BitString k) (T : ℕ) (u : Circuit signature (m + k) (m + k)) (hu : u.Computes interpretation (prodMap U P)^[T]) : ∃ (d : Circuit signature m m), d.Computes interpretation U^[T] ∧ d.size ≤ u.size + 2

Each power of a product map is at least as hard as the same power of its first factor.

Group actions by a hardwired element

theorem Cslib.Circuits.Boolean.Iteration.smul_perm_symm {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) : ⇑(Equiv.symm (MulAction.toPerm g)) = fun (x : α) => g⁻¹ • x

The permutation x ↦ g • x of a group action has inverse x ↦ g⁻¹ • x.

theorem Cslib.Circuits.Boolean.Iteration.smul_zpow_circuit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {k n : ℕ} (encG : G → BitString k) (enc : α → BitString n) (act : Circuit signature (k + n) n) (hact : ∀ (g : G) (x : α), act.eval interpretation (Fin.append (encG g) (enc x)) = enc (g • x)) (g : G) (T : ℤ) : ∃ (d : Circuit signature n n), (∀ (x : α), d.eval interpretation (enc x) = enc (g ^ T • x)) ∧ d.size ≤ act.size + 2

If a circuit evaluates a group action on encodings of elements and points, every integer power of the action of a fixed element, including the inverse permutation, has a circuit with at most two more gates.

theorem Cslib.Circuits.Boolean.Iteration.smul_iterate_circuit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {k n : ℕ} (encG : G → BitString k) (enc : α → BitString n) (act : Circuit signature (k + n) n) (hact : ∀ (g : G) (x : α), act.eval interpretation (Fin.append (encG g) (enc x)) = enc (g • x)) (g : G) (T : ℕ) : ∃ (d : Circuit signature n n), (∀ (x : α), d.eval interpretation (enc x) = enc ((fun (y : α) => g • y)^[T] x)) ∧ d.size ≤ act.size + 2

Every power of the action of a fixed element, as an iterate.

theorem Cslib.Circuits.Boolean.Iteration.smul_inverse_circuit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {k n : ℕ} (encG : G → BitString k) (enc : α → BitString n) (act : Circuit signature (k + n) n) (hact : ∀ (g : G) (x : α), act.eval interpretation (Fin.append (encG g) (enc x)) = enc (g • x)) (g : G) : ∃ (d : Circuit signature n n), (∀ (x : α), d.eval interpretation (enc x) = enc ((Equiv.symm (MulAction.toPerm g)) x)) ∧ d.size ≤ act.size + 2

The inverse of the action of a fixed element.

theorem Cslib.Circuits.Boolean.Iteration.pairAction_iterate {G : Type u_1} {α : Type u_2} [Monoid G] [MulAction G α] (t : ℕ) (g : G) (x : α) : (fun (p : G × α) => (p.1, p.1 • p.2))^[t] (g, x) = (g, g ^ t • x)

The iterator of (g, x) ↦ (g, g • x) raises the carried element to the tth power.

A universal step map

structure Cslib.Circuits.Boolean.Iteration.Universal.Description (σ : Signature) (n G : ℕ) : Type v

A straight-line program held in the state: each of G entries is an operation with operand indices, and outputs lists the wires copied back to the input registers. Index i < n names input i, and index n + j names work register j.

• entries : Fin G → (op : σ.Op) × (Fin (σ.Arity op) → ℕ)

  The G gate entries, each pairing an operation with its operand wire indices.

• outputs : Fin n → ℕ

  The indices of the wires copied back into the n input registers after a round.

structure Cslib.Circuits.Boolean.Iteration.Universal.Config (σ : Signature) (V : Type w) (n G : ℕ) : Type (max v w)

A state of the universal map: the program, the input registers, the work registers, and an unbounded natural-number program counter. Because desc carries natural-number wire indices and pc : ℕ, this is an infinite mathematical configuration space rather than a finite Boolean state space.

• desc : Description σ n G

  The straight-line program description held in the state.

• x : Fin n → V

  The n input registers.

• w : Fin G → V

  The G work registers.

• pc : ℕ

  The program counter.

def Cslib.Circuits.Boolean.Iteration.Universal.read {V : Type w} [Inhabited V] {n G : ℕ} (x : Fin n → V) (w : Fin G → V) (i : ℕ) : V

Read the register with a given index. Indices out of range read the default value of V.

def Cslib.Circuits.Boolean.Iteration.Universal.step {σ : Signature} {V : Type w} [Inhabited V] {n G : ℕ} (I : Interpretation σ V) (s : Config σ V n G) : Config σ V n G

One semantic step: evaluate entry pc into work register pc, or, when pc ≥ G, simultaneously copy the outputs into the input registers, clear the work registers to default, and reset the counter.

def Cslib.Circuits.Boolean.Iteration.Universal.wireIndex {n g : ℕ} : Wire n g → ℕ

The index of a CSLib wire.

def Cslib.Circuits.Boolean.Iteration.Universal.describe {σ : Signature} {n : ℕ} (G : ℕ) (c : Circuit σ n n) (pad : σ.Op) : Description σ n G

The description of a circuit with at most G gates, padded by copies of pad.

def Cslib.Circuits.Boolean.Iteration.Universal.start {σ : Signature} {V : Type w} [Inhabited V] {n G : ℕ} (D : Description σ n G) (x : Fin n → V) : Config σ V n G

The start state on input x.

theorem Cslib.Circuits.Boolean.Iteration.Universal.lines_wire_lt {σ : Signature} {n g : ℕ} (p : Program σ n g) (j : Fin g) (a : Fin (σ.Arity (p.lines j).op)) (b : Fin g) : (p.lines j).wires a = Wire.gate b → ↑b < ↑j

The widened lines of a program read only earlier gates.

theorem Cslib.Circuits.Boolean.Iteration.Universal.read_wireIndex {V : Type w} [Inhabited V] {n G g : ℕ} (x : Fin n → V) (w : Fin G → V) (e : Fin g → V) (wire : Wire n g) (hlt : ∀ (b : Fin g), wire = Wire.gate b → ↑b < G) (hw : ∀ (b : Fin g) (h : ↑b < G), wire = Wire.gate b → w ⟨↑b, h⟩ = e b) : read x w (wireIndex wire) = Wire.elim x e wire

Reading a wire by its index, from work registers that hold the gate values.

theorem Cslib.Circuits.Boolean.Iteration.Universal.run {σ : Signature} {V : Type w} [Inhabited V] {n G : ℕ} (I : Interpretation σ V) (c : Circuit σ n n) (pad : σ.Op) (hG : c.size ≤ G) (x : Fin n → V) (k : ℕ) : k ≤ G → ∃ (w : Fin G → V), (step I)^[k] (start (describe G c pad) x) = { desc := describe G c pad, x := x, w := w, pc := k } ∧ ∀ (j : Fin G), ↑j < k → ∀ (hs : ↑j < c.size), w j = c.program.eval I x ⟨↑j, hs⟩

After k ≤ G steps from the start state, the first k work registers hold the values of the corresponding gates.

theorem Cslib.Circuits.Boolean.Iteration.Universal.step_round {σ : Signature} {V : Type w} [Inhabited V] {n G : ℕ} (I : Interpretation σ V) (c : Circuit σ n n) (pad : σ.Op) (hG : c.size ≤ G) (x : Fin n → V) : (step I)^[G + 1] (start (describe G c pad) x) = start (describe G c pad) (c.eval I x)

One round of G + 1 steps of the universal map runs a circuit with at most G gates and returns to a start state.

theorem Cslib.Circuits.Boolean.Iteration.Universal.step_iterate {σ : Signature} {V : Type w} [Inhabited V] {n G : ℕ} (I : Interpretation σ V) (c : Circuit σ n n) (pad : σ.Op) (hG : c.size ≤ G) (T : ℕ) (x : Fin n → V) : (step I)^[(G + 1) * T] (start (describe G c pad) x) = start (describe G c pad) ((c.eval I)^[T] x)

(G + 1) * T steps of the universal map run T rounds of the circuit.

theorem Cslib.Circuits.Boolean.Iteration.Universal.universal_power_circuit {n G m : ℕ} (c : Circuit signature n n) (pad : signature.Op) (hG : c.size ≤ G) (e : Config signature Bool n G → BitString m) (place : Fin m → Fin n ⊕ Bool) (select : Fin n → Fin m) (hsel : ∀ (i : Fin n), place (select i) = Sum.inl i) (he : ∀ (x : Fin n → Bool), e (start (describe G c pad) x) = hardwired place x) (T : ℕ) (u : Circuit signature m m) (hu : ∀ (x : Fin n → Bool), u.eval interpretation (e (start (describe G c pad) x)) = e ((step interpretation)^[(G + 1) * T] (start (describe G c pad) x))) : ∃ (d : Circuit signature n n), d.Computes interpretation (c.eval interpretation)^[T] ∧ d.size ≤ u.size + 2

The conditional circuit consequence: assuming a bit encoding e of universal-map states that writes the input registers of a start state directly and fixes its other bits to constants determined by the description (he), together with a circuit u for the (G + 1) * T-th power of Universal.step on those start states (hu), one obtains a circuit for the Tth power of c with at most two more gates. Neither e nor a circuit for one universal step is constructed here.