The modular-counter permutation: exponential lower bounds and typical powers

Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Basic.lean defines the single-step modular-counter permutation counterStep k on 2 k bits (ModulusCounter.power 1), constructs its linear-size De Morgan circuit of size at most 50 * k + 20, and proves that its powers below ModulusCounter.period k = lcm(1, …, 2 ^ k - 1) are pairwise distinct. Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Remainders.lean relates counter powers to integer remainders and short-exponent circuits.

By Chebyshev's lower bound on lcmUpto (2 ^ k - 1) and the ordered-syntax circuit count from CircuitCounting.lean, this file proves that for every k ≥ 64:

• some exponent T < ModulusCounter.period k requires more than lowerBudget k = 2 ^ k / (1024 * (k + 1)) gates (exists_hard_counter_power, counter_power_lower_bound), matching the 2 ^ Θ(n) fixed-power upper bound up to the constant factor in the exponent;
• at most a 2 ^ (-2 ^ (k - 1)) fraction of exponents below ModulusCounter.period k have circuits of size at most lowerBudget k (almost_all_counter_powers_hard, counter_powers_average_complexity).

Main definitions

• Cslib.Circuits.Boolean.Iteration.easyCounterPowers, Cslib.Circuits.Boolean.Iteration.hardCounterPowers: exponents below period k computable with at most q gates, and those requiring more than q gates.

Main results

• Cslib.Circuits.Boolean.Iteration.description_budget_lt_period: the De Morgan description budget at lowerBudget k is strictly smaller than ModulusCounter.period k for k ≥ 64.
• Cslib.Circuits.Boolean.Iteration.exists_hard_counter_power, Cslib.Circuits.Boolean.Iteration.counter_power_lower_bound: for k ≥ 64, counterStep k has a power requiring more than 2 ^ k / (1024 * (k + 1)) gates.
• Cslib.Circuits.Boolean.Iteration.almost_all_counter_powers_hard, Cslib.Circuits.Boolean.Iteration.counter_powers_average_complexity: all but a 2 ^ (-2 ^ (k - 1)) fraction of powers below period k require more than lowerBudget k gates.
• Cslib.Circuits.Boolean.Iteration.distinct_counter_powers_up_to, Cslib.Circuits.Boolean.Iteration.exists_hard_counter_power_up_to: counting lower bound for prefixes T < M ≤ period k.

References

• Adapted from lean/Proofs/{LowerBound,TypicalPowers}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Worst-case and typical-power lower bounds

theorem Cslib.Circuits.Boolean.Iteration.description_budget_lt_period (k : ℕ) (hk : 64 ≤ k) : signature.orderedBudget (k + k) (k + k) (lowerBudget k) < ModulusCounter.period k

The De Morgan description budget for lowerBudget k gates is strictly smaller than ModulusCounter.period k for k ≥ 64.

theorem Cslib.Circuits.Boolean.Iteration.exists_hard_counter_power (k : ℕ) (hk : 64 ≤ k) : ∃ T < ModulusCounter.period k, ∀ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (ModulusCounter.power T) → lowerBudget k < out.size

For every k ≥ 64, some exponent T < ModulusCounter.period k requires more than lowerBudget k gates.

theorem Cslib.Circuits.Boolean.Iteration.counter_power_lower_bound (k : ℕ) (hk : 64 ≤ k) : ∃ (c : Circuit signature (k + k) (k + k)), c.size ≤ 50 * (k + 1) ∧ Function.Bijective (c.eval interpretation) ∧ ∃ T < ModulusCounter.period k, ∀ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (c.eval interpretation)^[T] → 2 ^ k / (1024 * (k + 1)) < out.size

Matching exponential lower bound. For every k ≥ 64, there is a bijective circuit c on 2 k bits of size at most 50 * (k + 1) with a power c^[T] (T < ModulusCounter.period k) requiring more than 2 ^ k / (1024 * (k + 1)) gates.

noncomputable def Cslib.Circuits.Boolean.Iteration.easyCounterPowers (k q : ℕ) : Finset (Fin (ModulusCounter.period k))

Exponents below ModulusCounter.period k whose power has a circuit of size at most q.

noncomputable def Cslib.Circuits.Boolean.Iteration.hardCounterPowers (k q : ℕ) : Finset (Fin (ModulusCounter.period k))

Exponents below ModulusCounter.period k whose power requires more than q gates.

theorem Cslib.Circuits.Boolean.Iteration.mem_easyCounterPowers (k q : ℕ) (T : Fin (ModulusCounter.period k)) : T ∈ easyCounterPowers k q ↔ ∃ (c : Circuit signature (k + k) (k + k)), c.size ≤ q ∧ c.Computes interpretation (ModulusCounter.power ↑T)

theorem Cslib.Circuits.Boolean.Iteration.easyCounterPowers_card_le (k q : ℕ) : (easyCounterPowers k q).card ≤ signature.orderedBudget (k + k) (k + k) q

theorem Cslib.Circuits.Boolean.Iteration.hardCounterPowers_card_ge (k q : ℕ) : ModulusCounter.period k - signature.orderedBudget (k + k) (k + k) q ≤ (hardCounterPowers k q).card

theorem Cslib.Circuits.Boolean.Iteration.lowerBudget_description_margin (k : ℕ) (hk : 64 ≤ k) : have q := lowerBudget k; 3 * q + (k + 2) * (2 * q + (k + k) + 1) + k + 2 ^ (k - 1) ≤ 2 ^ k - 1

The description budget at lowerBudget k leaves an additive margin of 2 ^ (k - 1) in the binary exponent.

theorem Cslib.Circuits.Boolean.Iteration.almost_all_counter_powers_hard (k : ℕ) (hk : 64 ≤ k) : (easyCounterPowers k (lowerBudget k)).card * 2 ^ 2 ^ (k - 1) ≤ ModulusCounter.period k

Almost every counter power is hard. At most a 2 ^ (-2 ^ (k - 1)) fraction of exponents below ModulusCounter.period k have circuits of size at most lowerBudget k.

theorem Cslib.Circuits.Boolean.Iteration.counter_powers_average_complexity (k : ℕ) (hk : 64 ≤ k) : ModulusCounter.period k < 2 * (hardCounterPowers k (lowerBudget k)).card

For k ≥ 64, more than half of the exponents below ModulusCounter.period k lie in hardCounterPowers k (lowerBudget k).

theorem Cslib.Circuits.Boolean.Iteration.distinct_counter_powers_up_to {k M : ℕ} (hM : M ≤ ModulusCounter.period k) : Function.Injective fun (T : Fin M) => ModulusCounter.power ↑T

All powers ModulusCounter.power T for T < M with M ≤ ModulusCounter.period k are pairwise distinct.

theorem Cslib.Circuits.Boolean.Iteration.exists_hard_counter_power_up_to {k M q : ℕ} (hM : M ≤ ModulusCounter.period k) (large : signature.orderedBudget (k + k) (k + k) q < M) : ∃ T < M, ∀ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (ModulusCounter.power T) → q < out.size

If signature.orderedBudget (k + k) (k + k) q < M and M ≤ ModulusCounter.period k, some exponent T < M requires more than q gates.