Asymptotic coefficient synthesis for affine controllers

Applying Lupanov's scalar synthesis theorem to the controller output and the coefficients of the composed affine payload gives, for every ε > 0 and sufficiently large controller width q, the fixed-power circuit bound

(q + p * (p + 1)) * ((1 + ε) * 2 ^ q / q) + p * (5 * (p + 1) + 1).

The threshold on q is uniform in the payload width p, controller, affine maps and fixed exponent. The final summand charges one matrix-vector multiplication and translation. Binary powering gives the corresponding bound for an input exponent of m bits.

These are nonuniform circuit-size bounds in the same De Morgan model as affine_controller_power; no construction-time bound or new synthesis theorem is claimed. This applies the classical scalar synthesis bound to the existing affine-controller decomposition; no priority claim is made.

Main results

• Cslib.Circuits.Boolean.Iteration.affine_controller_power_lupanov: a fixed exponent.
• Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_lupanov: an input exponent.

References

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

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_power_lupanov (ε : ℝ) (hε : 0 < ε) : ∃ (q₀ : ℕ), ∀ q ≥ 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 ≤ ↑(q + p * (p + 1)) * ((1 + ε) * 2 ^ q / ↑q) + ↑(p * (5 * (p + 1) + 1))

Lupanov synthesis gives an asymptotic coefficient of one for the controller-output and affine-coefficient tables, uniformly in the payload width and fixed exponent.

theorem Cslib.Circuits.Boolean.Iteration.affine_controller_variable_time_lupanov (ε : ℝ) (hε : 0 < ε) : ∃ (q₀ : ℕ), ∀ q ≥ 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 * (↑(q + p * (p + 1)) * ((1 + ε) * 2 ^ q / ↑q) + ↑(p * (5 * (p + 1) + 1)) + ↑(4 * (q + p)))

The same asymptotic coefficient-synthesis bound at each conditional binary stage computes an input exponent with m bits.