Documentation

Complexity.Computability.Circuit.Boolean.Iteration.Active

Fixed powers charged to long trajectories #

The storage term of the fixed-power bound counts all 2 ^ n states. It suffices to count the active states: those of transient depth at least L and those on cycles of length at least L (FunctionalGraph.activeVertices). Checkpoints packed inside the active set cover every orbit within 4 L steps (FunctionalGraph.exists_active_checkpoints), so the fixed-power construction with an orbit prefix of 4 L states gives a circuit of size at most 120000 * powerBudget n s Q L, where Q is the number of active states for this L (active_mass_fixed_power). The count Q depends on L.

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. The checkpoints are chosen nonconstructively, so the circuits exist for each T and L; nothing here bounds the time to construct them.

Main results #

References #

source
theorem Cslib.Circuits.Boolean.Iteration.active_construction_cost (n s M L d : ℕ) (hL : 0 < L) (hd : d ≤ n + 3) (hR : 2 ^ d ≤ 2 * (M + 4 * L + 1)) :
2 + 5 * (4 * L) * s + (18 * d ^ 2 + 30) * 2 ^ d * (Record.width n (n + 3) + 1) + 1000 * (4 * L + 1) * (n + (n + 3) + 1) ^ 2 ≤ 120000 * (L * s + (n + 1) ^ 3 * (L + M + 1))
source
theorem Cslib.Circuits.Boolean.Iteration.active_mass_fixed_power (n : ℕ) (c : Circuit signature n n) (T L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) :
∃ (out : Circuit signature n n), out.Computes interpretation (c.eval interpretation)^[T] ∧ out.size ≤ 120000 * powerBudget n c.size (FunctionalGraph.activeVertices (c.eval interpretation) L).card L

Fixed powers charged to long trajectories. For every exponent T and every 0 < L ≤ 2 ^ n, some circuit of size at most 120000 * powerBudget n c.size Q L computes T applications of c, where Q is the number of states of transient depth at least L or on cycles of length at least L.