Optimizing the checkpoint parameter

Balancing the two terms of powerBudget over the integer parameter L gives a fixed-power circuit of size at most 120000 * (s' + √((n + 1) ^ 3 * M * s')) with s' = s + (n + 1) ^ 3 (fixed_power_on_optimized): rounding the real balancing point costs a factor three. In particular every fixed power has a circuit of size at most 120000 * (s + (n + 1) ^ 3) * 2 ^ ((n + 1) / 2) (fixed_power_half_exponent), and transition circuits of polynomial size give fixed powers of polynomial times half-exponential size (fixed_power_polynomial).

Main definitions

• Cslib.Circuits.Boolean.Iteration.optimizedBudget: the balanced square-root budget.

Main results

• Cslib.Circuits.Boolean.Iteration.fixed_power_optimized, fixed_power_on_optimized: the square-root bounds.
• Cslib.Circuits.Boolean.Iteration.fixed_power_half_exponent: a closed-form bound.
• Cslib.Circuits.Boolean.Iteration.fixed_power_polynomial: polynomial transition circuits.

References

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

noncomputable def Cslib.Circuits.Boolean.Iteration.optimizedBudget (n s M : ℕ) : ℝ

The balanced budget s' + √((n + 1) ^ 3 * M * s') with s' = s + (n + 1) ^ 3.

theorem Cslib.Circuits.Boolean.Iteration.exists_le_three_mul_add_sqrt (a b M N : ℕ) (hb : 0 < b) (hba : b ≤ a) (hMN : M ≤ N) (hN : 0 < N) : ∃ (L : ℕ), 0 < L ∧ L ≤ N ∧ ↑(a * L + b * (M / L + 1)) ≤ 3 * (↑a + √(↑b * ↑M * ↑a))

Rounding the balancing point of a * L + b * (M / L + 1) costs at most a factor three.

theorem Cslib.Circuits.Boolean.Iteration.exists_powerBudget_le_optimizedBudget (n s M : ℕ) (hM : M ≤ 2 ^ n) : ∃ (L : ℕ), 0 < L ∧ L ≤ 2 ^ n ∧ ↑(powerBudget n s M L) ≤ 3 * optimizedBudget n s M

For any M ≤ 2 ^ n, there is a checkpoint parameter 0 < L ≤ 2 ^ n with powerBudget n s M L ≤ 3 * optimizedBudget n s M.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_optimized {n : ℕ} (c : Circuit signature n n) (T : ℕ) : ∃ (out : Circuit signature n n), out.Computes interpretation (c.eval interpretation)^[T] ∧ ↑out.size ≤ 120000 * optimizedBudget n c.size (2 ^ n)

Square-root fixed powers.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_on_optimized {n : ℕ} (c : Circuit signature n n) (S : Finset (BitString n)) (hS : ∀ x ∈ S, c.eval interpretation x ∈ S) (T : ℕ) : ∃ (out : Circuit signature n n), out.ComputesOn interpretation (↑S) (c.eval interpretation)^[T] ∧ ↑out.size ≤ 120000 * optimizedBudget n c.size S.card

Square-root fixed powers on an invariant set.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_half_exponent {n : ℕ} (c : Circuit signature n n) (T : ℕ) : ∃ (out : Circuit signature n n), out.Computes interpretation (c.eval interpretation)^[T] ∧ out.size ≤ 120000 * (c.size + (n + 1) ^ 3) * 2 ^ ((n + 1) / 2)

A closed-form half-exponential bound.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_polynomial {n : ℕ} (c : Circuit signature n n) (K d T : ℕ) (hs : c.size ≤ K * (n + 1) ^ d) : ∃ (out : Circuit signature n n), out.Computes interpretation (c.eval interpretation)^[T] ∧ out.size ≤ 120000 * (K + 1) * (n + 1) ^ max d 3 * 2 ^ ((n + 1) / 2)

Transition circuits of size K * (n + 1) ^ d give fixed powers of size 120000 * (K + 1) * (n + 1) ^ max d 3 * 2 ^ ((n + 1) / 2).