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

• Cslib.Circuits.Boolean.Iteration.active_mass_fixed_power: fixed powers charged to the active states.

References

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

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.