Autonomous controllers and affine-payload iteration bounds

When a state splits into an autonomous controller and a payload (controlledMap), the controller evolves independently of the payload and each step applies a controller-selected transformation to the payload. Iterating for T steps therefore applies g^[T] to the controller and the composite payload map controlledPayload g a T u to the payload (controlledMap_iterate, controlledBits_iterate). Whenever the payload maps belong to a composition-closed family containing the identity, every iterate's payload map remains in that family (controlledPayload_mem).

On q controller bits and p payload bits (controlledBits), if every payload transformation in a composition-closed family has a Boolean circuit of size at most K, then every fixed iterate (controlledBits g a)^[T] has a circuit of size at most 2 + 2 ^ q * (K + 6 * q + 4 * p + 1) (controlled_family_power), and an m-bit input time costs at most m * (2 + 2 ^ q * (K + 6 * q + 4 * p + 1) + 4 * (q + p)) (controlled_family_variable_time). No circuit for the controller transition g is assumed or needed: the circuit enumerates all 2 ^ q controller states, hardwires g^[T] u, runs the circuit for controlledPayload g a T u, and selects the active record.

In particular, affine maps BitString p →ᵃ[Bool] BitString p over Bool are closed under composition and are computed by circuits of size at most p * (5 * (p + 1) + 1) via their affine-hash representation (affineHash_circuit, affineHash_affineMapSeed, affine_payload_circuit). Every fixed iterate of an autonomous q-bit controller with a p-bit affine payload therefore has a circuit of size at most affineControllerBudget q p ≤ 32 * 2 ^ q * (q + p ^ 2 + 1) (affine_controller_power, affineControllerBudget_le), which is polynomial in the total width whenever 2 ^ q is (affine_controller_polynomial).

Main definitions

• Cslib.Circuits.Boolean.Iteration.controlledMap: product map with an autonomous controller and a controller-selected payload map.
• Cslib.Circuits.Boolean.Iteration.controlledPayload: composite payload transformation after T steps from a given initial controller state.
• Cslib.Circuits.Boolean.Iteration.controlledBits: flat bit-string encoding of a q-bit controller followed by a p-bit payload.
• Cslib.Circuits.Boolean.Iteration.affineMapSeed: matrix and offset seed representing a Boolean affine map as an affine hash.
• Cslib.Circuits.Boolean.Iteration.affineControllerBudget: exact gate budget for a q-bit autonomous controller with a p-bit affine payload.

Main results

• Cslib.Circuits.Boolean.Iteration.controlledMap_iterate, Cslib.Circuits.Boolean.Iteration.controlledBits_iterate: exact characterization of iterates of a controlled map.
• Cslib.Circuits.Boolean.Iteration.controlledPayload_mem: closure of composite payload maps in any composition-closed family.
• Cslib.Circuits.Boolean.Iteration.controlled_circuit, Cslib.Circuits.Boolean.Iteration.controlled_family_power, Cslib.Circuits.Boolean.Iteration.controlled_family_variable_time: circuit size bounds for selecting and iterating bounded-cost payload families.
• Cslib.Circuits.Boolean.Iteration.affineHash_circuit, Cslib.Circuits.Boolean.Iteration.affine_payload_circuit: quadratic-size circuits for affine hashes and Boolean affine maps.
• Cslib.Circuits.Boolean.Iteration.affine_controller_power, Cslib.Circuits.Boolean.Iteration.affineControllerBudget_le, Cslib.Circuits.Boolean.Iteration.affine_controller_polynomial, Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time: fixed-power, polynomial, and input-time circuit bounds for autonomous controllers with affine payloads.

References

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

Autonomous controllers and composite payloads

def Cslib.Circuits.Boolean.Iteration.controlledMap {α : Type u} {β : Type v} (g : α → α) (a : α → β → β) (x : α × β) : α × β

An autonomous controller chooses the transformation of a payload.

def Cslib.Circuits.Boolean.Iteration.controlledPayload {α : Type u} {β : Type v} (g : α → α) (a : α → β → β) : ℕ → α → β → β

The composite payload map selected by an initial controller and fixed time.

theorem Cslib.Circuits.Boolean.Iteration.controlledMap_iterate {α : Type u} {β : Type v} (g : α → α) (a : α → β → β) (T : ℕ) (u : α) (v : β) : (controlledMap g a)^[T] (u, v) = (g^[T] u, controlledPayload g a T u v)

Iterating a controlled map advances the autonomous controller and applies the composite payload map.

theorem Cslib.Circuits.Boolean.Iteration.controlledPayload_mem {α : Type u} {β : Type v} (g : α → α) (a : α → β → β) (family : Set (β → β)) (hid : id ∈ family) (hcomp : ∀ f ∈ family, ∀ h ∈ family, f ∘ h ∈ family) (ha : ∀ (u : α), a u ∈ family) (T : ℕ) (u : α) : controlledPayload g a T u ∈ family

Composition closure suffices semantically, without any finite-state hypothesis.

def Cslib.Circuits.Boolean.Iteration.controlledBits {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (x : BitString (q + p)) : BitString (q + p)

Flat Boolean encoding of a q-bit controller followed by a p-bit payload.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.controlledBits_append {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (u : BitString q) (v : BitString p) : controlledBits g a (Fin.append u v) = Fin.append (g u) (a u v)

theorem Cslib.Circuits.Boolean.Iteration.controlledBits_iterate {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (T : ℕ) (x : BitString (q + p)) : (controlledBits g a)^[T] x = controlledBits g^[T] (controlledPayload g a T) x

Iterating controlledBits is controlledBits with the iterated controller and composite payload map.

Selecting and powering bounded-cost payload families

theorem Cslib.Circuits.Boolean.Iteration.controlled_circuit {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (K : ℕ) (ha : ∀ (u : BitString q), ∃ (c : Circuit signature p p), c.Computes interpretation (a u) ∧ c.size ≤ K) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g a) ∧ c.size ≤ 2 + 2 ^ q * (K + 6 * q + 4 * p + 1)

Selecting among small payload circuits has overhead linear in controller and output width per controller value. No circuit for g is assumed or needed.

theorem Cslib.Circuits.Boolean.Iteration.controlled_family_power {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (family : Set (BitString p → BitString p)) (hid : id ∈ family) (hcomp : ∀ f ∈ family, ∀ h ∈ family, f ∘ h ∈ family) (ha : ∀ (u : BitString q), a u ∈ family) (K : ℕ) (hK : ∀ f ∈ family, ∃ (c : Circuit signature p p), c.Computes interpretation f ∧ c.size ≤ K) (T : ℕ) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g a)^[T] ∧ c.size ≤ 2 + 2 ^ q * (K + 6 * q + 4 * p + 1)

A composition-closed payload family with a uniform gate bound can be powered at a cost exponential only in the controller width.

theorem Cslib.Circuits.Boolean.Iteration.controlled_family_variable_time {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (family : Set (BitString p → BitString p)) (hid : id ∈ family) (hcomp : ∀ f ∈ family, ∀ h ∈ family, f ∘ h ∈ family) (ha : ∀ (u : BitString q), a u ∈ family) (K : ℕ) (hK : ∀ f ∈ family, ∃ (c : Circuit signature p p), c.Computes interpretation f ∧ c.size ≤ K) (m : ℕ) : ∃ (c : Circuit signature (q + p + m) (q + p)), c.Computes interpretation (inputTimeIterate (controlledBits g a) m) ∧ c.size ≤ m * (2 + 2 ^ q * (K + 6 * q + 4 * p + 1) + 4 * (q + p))

The same closed family supports an input exponent by conditional binary powers.

Affine payloads and affine-controller bounds

theorem Cslib.Circuits.Boolean.Iteration.affineHash_circuit {k n : ℕ} (seed : (Fin k → BitString n) × BitString k) : ∃ (c : Circuit signature n k), c.Computes interpretation (BitString.LinearHash.affineHash seed) ∧ c.size ≤ k * (5 * (n + 1) + 1)

Every affine hash x ↦ A x + b from n bits to k bits has a De Morgan circuit of size at most k * (5 * (n + 1) + 1).

def Cslib.Circuits.Boolean.Iteration.affineMapSeed {p : ℕ} (a : BitString p →ᵃ[Bool] BitString p) : (Fin p → BitString p) × BitString p

The matrix and offset seed of a Boolean affine map.

theorem Cslib.Circuits.Boolean.Iteration.affineHash_affineMapSeed {p : ℕ} (a : BitString p →ᵃ[Bool] BitString p) (v : BitString p) : BitString.LinearHash.affineHash (affineMapSeed a) v = a v

Evaluating the affine hash at affineMapSeed a recovers the affine map a.

theorem Cslib.Circuits.Boolean.Iteration.affine_payload_circuit {p : ℕ} (a : BitString p →ᵃ[Bool] BitString p) : ∃ (c : Circuit signature p p), c.Computes interpretation ⇑a ∧ c.size ≤ p * (5 * (p + 1) + 1)

Every affine Boolean payload has a De Morgan circuit of size at most p * (5 * (p + 1) + 1).

def Cslib.Circuits.Boolean.Iteration.affineControllerBudget (q p : ℕ) : ℕ

Exact gate budget from affine payload evaluation and autonomous controller selection.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_power {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (T : ℕ) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g fun (u : BitString q) => ⇑(a u))^[T] ∧ c.size ≤ affineControllerBudget q p

Every fixed power has size exponential only in the autonomous controller width.

theorem Cslib.Circuits.Boolean.Iteration.affineControllerBudget_le (q p : ℕ) : affineControllerBudget q p ≤ 32 * 2 ^ q * (q + p ^ 2 + 1)

The exact budget is O(2 ^ q * (q + p ^ 2 + 1)), including zero-width cases.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_polynomial {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (K d : ℕ) (hcontroller : 2 ^ q ≤ K * (q + p + 1) ^ d) (T : ℕ) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g fun (u : BitString q) => ⇑(a u))^[T] ∧ c.size ≤ 32 * K * (q + p + 1) ^ (d + 2)

Polynomially many controller states give a polynomial gate bound in the total width, uniformly over all fixed exponents.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (m : ℕ) : ∃ (c : Circuit signature (q + p + m) (q + p)), c.Computes interpretation (inputTimeIterate (controlledBits g fun (u : BitString q) => ⇑(a u)) m) ∧ c.size ≤ m * (affineControllerBudget q p + 4 * (q + p))

An input time uses the same fixed-power bound at each conditional binary stage.