Synthesizing the coefficients of an affine controller

For an autonomous q-bit controller with a p-bit affine payload, every fixed iterate is again a controller-selected affine map. Its q controller outputs and p * (p + 1) matrix and offset coefficients are Boolean functions of only the controller input. Synthesizing these coefficient functions before applying the affine map costs (q + p * (p + 1)) * L + p * (5 * (p + 1) + 1) gates whenever every Boolean function on q inputs has a circuit with at most L gates.

The finite Shannon bound gives L = 27 * 2 ^ q / q for q ≥ 16. In particular, when p = q, this improves the existing O(q ^ 2 * 2 ^ q) bound from separate affine maps for all controller states to O(q * 2 ^ q). The hypotheses on the controller and affine payloads are unchanged. Binary powering transfers the improvement to input-time iteration.

This combines the existing controller decomposition and classical Boolean synthesis. It is a strengthening of the library's affine-controller bound; no priority or optimality claim is made. All NOT, AND, OR and constant gates are charged, while wiring and fanout are free. These are nonuniform circuit-size bounds, with no bound on the time needed to construct the circuits or their coefficient tables.

Main definitions

• Cslib.Circuits.Boolean.Iteration.affineControllerSynthesisBudget: the coefficient-table synthesis budget, parameterized by the scalar Boolean synthesis bound.

Main results

• Cslib.Circuits.Boolean.Iteration.controlled_affine_circuit_of_scalar_bound: synthesize an arbitrary controller-selected affine map.
• Cslib.Circuits.Boolean.Iteration.affine_controller_power_of_scalar_bound: every fixed iterate satisfies the same budget.
• Cslib.Circuits.Boolean.Iteration.affine_controller_power_shannon: the finite bound using 27 * 2 ^ q / q gates per coefficient, for q ≥ 16.
• Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_of_scalar_bound, Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_shannon: input-time bounds.

References

• [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f], for the existing affine-controller decomposition.
• O. B. Lupanov, On a Method of Circuit Synthesis, for Boolean synthesis.

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

Synthesizing the controller output and affine coefficients at L gates each, followed by one affine evaluation.

theorem Cslib.Circuits.Boolean.Iteration.controlled_affine_circuit_of_scalar_bound {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (L : ℕ) (hL : ∀ (f : BooleanFunction q), ∃ (c : Circuit signature q 1), c.Computes interpretation (single f) ∧ c.size ≤ L) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g fun (u : BitString q) => ⇑(a u)) ∧ c.size ≤ affineControllerSynthesisBudget q p L

Compute a controller-selected affine map by synthesizing its scalar coefficients. This accepts any size bound valid for all q-input Boolean functions.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_power_of_scalar_bound {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (L : ℕ) (hL : ∀ (f : BooleanFunction q), ∃ (c : Circuit signature q 1), c.Computes interpretation (single f) ∧ c.size ≤ L) (T : ℕ) : ∃ (c : Circuit signature (q + p) (q + p)), c.Computes interpretation (controlledBits g fun (u : BitString q) => ⇑(a u))^[T] ∧ c.size ≤ affineControllerSynthesisBudget q p L

Every fixed iterate has the coefficient-synthesis bound, since the composed payload map is affine for each initial controller state.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_power_shannon {q p : ℕ} (hq : 16 ≤ q) (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 ≤ affineControllerSynthesisBudget q p (27 * 2 ^ q / q)

Finite coefficient synthesis for controllers of width at least 16.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_of_scalar_bound {q p : ℕ} (g : BitString q → BitString q) (a : BitString q → BitString p →ᵃ[Bool] BitString p) (L : ℕ) (hL : ∀ (f : BooleanFunction q), ∃ (c : Circuit signature q 1), c.Computes interpretation (single f) ∧ c.size ≤ L) (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 * (affineControllerSynthesisBudget q p L + 4 * (q + p))

Conditional binary powers transfer any scalar synthesis bound to an input exponent.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_shannon {q p : ℕ} (hq : 16 ≤ q) (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 * (affineControllerSynthesisBudget q p (27 * 2 ^ q / q) + 4 * (q + p))

An input exponent with m bits, using the finite Shannon coefficient bound.