Circuits for fixed powers

Let c be a Boolean circuit with n inputs and n outputs of size s, computing a map f on n-bit states. Every fixed power f^[T] has a circuit of size at most 40000 * (L * s + (n + 1) ^ 3 * (L + 2 ^ n / L + 1)) for every 0 < L ≤ 2 ^ n (fixed_power). More precisely, on a finite set S of states with f '' S ⊆ S, a circuit of size at most 40000 * powerBudget n s S.card L agrees with f^[T] on S (fixed_power_on); powerBudget n s M L = L * s + (n + 1) ^ 3 * (L + M / L + 1).

The construction follows [Sch26f]. Choose at most |S| / L checkpoints in S such that the first L states of every orbit from S repeat or reach a checkpoint within 2 L steps (FunctionalGraph.exists_checkpoints), and hardwire each checkpoint h together with f^[T - 2 L] h. On input x, compute the first 2 L + 1 states of the orbit with copies of c, sort them together with the checkpoints, and detect a collision. A checkpoint hit at time d gives f^[T] x after 2 L - d further steps of the stored state; a repeat gives it as a prefix state at the time congruent to T. Short exponents T < 2 L use T copies of c.

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

Main definitions

• Cslib.Circuits.Boolean.Iteration.powerBudget: the size tradeoff.
• Cslib.Circuits.Boolean.Iteration.FixedPowerOnBound, FixedPowerBound: the tradeoffs with some constant.

Main results

• Cslib.Circuits.Boolean.Iteration.fixed_power_on: the invariant-set bound with constant 40000.
• Cslib.Circuits.Boolean.Iteration.fixed_power: the bound on all states.

References

• Adapted from lean/Statement.lean and lean/Proofs/{Construction,FixedPower}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.powerBudget (n s M L : ℕ) : ℕ

The fixed-power tradeoff L * s + (n + 1) ^ 3 * (L + M / L + 1) for states of n bits, a transition circuit of size s, M relevant states and parameter L.

def Cslib.Circuits.Boolean.Iteration.FixedPowerOnBound : Prop

Some constant C bounds a circuit for every fixed power on every invariant set by C * powerBudget.

def Cslib.Circuits.Boolean.Iteration.FixedPowerBound : Prop

Some constant C bounds a circuit for every fixed power by C * powerBudget with all 2 ^ n states.

theorem Cslib.Circuits.Boolean.Iteration.Record.initial_wires_subset {n w M : ℕ} (s : Set (BooleanFunction n)) (f : BitString n → BitString n) {R : ℕ} (T K : ℕ) (cp : Fin M → BitString n) (hp : prefixWires f K ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : (recordsWires fun (x : BitString n) => initial f T K cp x) ⊆ s

def Cslib.Circuits.Boolean.Iteration.fixedOutput {n w M : ℕ} (c : Circuit signature n n) (T K d : ℕ) (cp : Fin M → BitString n) (x : BitString n) : BitString n

The output of the fixed-power circuit for exponent T, prefix length K, sorting depth d and checkpoints cp.

theorem Cslib.Circuits.Boolean.Iteration.exists_fixedOutput {n w M : ℕ} (c : Circuit signature n n) (T K d : ℕ) (cp : Fin M → BitString n) : ∃ (out : Circuit signature n n), out.Computes interpretation (fixedOutput c T K d cp) ∧ out.size ≤ 2 + 5 * K * c.size + (18 * d ^ 2 + 30) * 2 ^ d * (Record.width n w + 1) + 1000 * (K + 1) * (n + w + 1) ^ 2

theorem Cslib.Circuits.Boolean.Iteration.construction_cost (n s M L d : ℕ) (hL : 0 < L) (hd : d ≤ n + 2) (hR : 2 ^ d ≤ 2 * (M + 2 * L + 1)) : 2 + 5 * (2 * L) * s + (18 * d ^ 2 + 30) * 2 ^ d * (Record.width n (n + 2) + 1) + 1000 * (2 * L + 1) * (n + (n + 2) + 1) ^ 2 ≤ 40000 * (L * s + (n + 1) ^ 3 * (L + M + 1))

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_on (n : ℕ) (c : Circuit signature n n) (S : Finset (BitString n)) (T L : ℕ) (hS : ∀ x ∈ S, c.eval interpretation x ∈ S) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), out.ComputesOn interpretation (↑S) (c.eval interpretation)^[T] ∧ out.size ≤ 40000 * powerBudget n c.size S.card L

Fixed powers on an invariant set. If c maps the finite set S into itself, then for every exponent T and every 0 < L ≤ 2 ^ n some circuit of size at most 40000 * powerBudget n c.size S.card L agrees with T applications of c on S.

theorem Cslib.Circuits.Boolean.Iteration.fixedPowerOnBound : FixedPowerOnBound

theorem Cslib.Circuits.Boolean.Iteration.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 ≤ 40000 * powerBudget n c.size (2 ^ n) L

Fixed powers. For every exponent T and every 0 < L ≤ 2 ^ n some circuit of size at most 40000 * powerBudget n c.size (2 ^ n) L computes T applications of c.

theorem Cslib.Circuits.Boolean.Iteration.fixedPowerBound : FixedPowerBound