Explicit description counts and hard powers for the native Boolean circuit model

For a finite signature σ, Signature.lineCount σ w counts the lines that can be formed from w available wires, and Signature.orderedBudget σ n m G counts the topologically ordered circuit descriptions with n inputs, m designated outputs, and at most G internal gates. Because every function in Circuit.functionsAtMost I n m G is computed by some such description, at most σ.orderedBudget n m G functions on n inputs and m outputs have circuits of size at most G (Circuit.card_functionsAtMost_le). Any finite family of functions larger than the ordered-syntax budget therefore contains a function requiring more than G gates (Circuit.exists_hard_in_family).

For the native De Morgan basis Boolean.signature (which charges constants, NOT, AND, and OR), boolean_lineCount_le bounds lineCount w by 5 * (w + 1) ^ 2, and boolean_orderedBudget_le and boolean_orderedBudget_le_pow bound orderedBudget n m q. Combining this with the exact number maxTransientDepth g + cyclePeriod g of distinct powers of a finite map g (FunctionalGraph.card_range_iterate) shows that whenever the ordered-syntax budget for q gates is smaller than maxTransientDepth g + cyclePeriod g, some power g^[T] with T < maxTransientDepth g + cyclePeriod g requires more than q gates (exists_hard_power_of_budget_lt, exists_hard_power).

Main definitions

• Cslib.Circuits.Signature.lineCount: number of lines over σ from w available wires.
• Cslib.Circuits.Signature.orderedBudget: number of topologically ordered circuits with n inputs, m outputs, and at most G gates.
• Cslib.Circuits.Circuit.functionsAtMost: functions computed by circuits of size at most G.
• Cslib.Circuits.Boolean.Iteration.lowerBudget: explicit exponential gate threshold 2 ^ k / (1024 * (k + 1)).

Main results

• Cslib.Circuits.Circuit.card_functionsAtMost_le: at most σ.orderedBudget n m G functions have circuits of size at most G.
• Cslib.Circuits.Circuit.exists_hard_in_family: a family larger than σ.orderedBudget n m G contains a function requiring more than G gates.
• Cslib.Circuits.Boolean.Iteration.boolean_lineCount_le, Cslib.Circuits.Boolean.Iteration.boolean_orderedBudget_le, Cslib.Circuits.Boolean.Iteration.boolean_orderedBudget_le_pow: explicit syntax bounds for the native De Morgan basis.
• Cslib.Circuits.Boolean.Iteration.exists_hard_power_of_budget_lt, Cslib.Circuits.Boolean.Iteration.exists_hard_power: existence of a hard power below maxTransientDepth g + cyclePeriod g.

References

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

def Cslib.Circuits.Signature.lineCount (σ : Signature) [Fintype σ.Op] (w : ℕ) : ℕ

Number of possible lines over σ when w wires are available.

theorem Cslib.Circuits.Line.card_eq_lineCount {σ : Signature} [Fintype σ.Op] (n g : ℕ) : Nat.card (Line σ n g) = σ.lineCount (n + g)

The number of lines with n inputs and g prior gates is σ.lineCount (n + g).

def Cslib.Circuits.Signature.orderedBudget (σ : Signature) [Fintype σ.Op] (n m G : ℕ) : ℕ

Number of topologically ordered circuit descriptions with n inputs, m designated outputs, and at most G internal gates.

noncomputable def Cslib.Circuits.Circuit.functionsAtMost {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n m G : ℕ) : Finset ((Fin n → U) → Fin m → U)

Functions from Fin n → U to Fin m → U computed by circuits with at most G gates.

theorem Cslib.Circuits.Circuit.mem_functionsAtMost_iff {σ : Signature} [Fintype σ.Op] {U : Type u} {I : Interpretation σ U} {n m G : ℕ} {target : (Fin n → U) → Fin m → U} : target ∈ functionsAtMost I n m G ↔ ∃ (c : Circuit σ n m), c.size ≤ G ∧ c.Computes I target

theorem Cslib.Circuits.Circuit.card_functionsAtMost_le {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) {n m G : ℕ} : (functionsAtMost I n m G).card ≤ σ.orderedBudget n m G

At most σ.orderedBudget n m G functions are computed by circuits of size at most G.

theorem Cslib.Circuits.Circuit.exists_hard_in_family {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) {n m G : ℕ} (family : Finset ((Fin n → U) → Fin m → U)) (large : σ.orderedBudget n m G < family.card) : ∃ target ∈ family, ∀ (c : Circuit σ n m), c.size ≤ G → ¬c.Computes I target

Any finite family of functions larger than σ.orderedBudget n m G contains a function requiring more than G gates.

theorem Cslib.Circuits.Boolean.Iteration.boolean_lineCount_le (w : ℕ) : signature.lineCount w ≤ 5 * (w + 1) ^ 2

Over the native De Morgan basis, at most 5 * (w + 1) ^ 2 lines can be formed from w available wires.

theorem Cslib.Circuits.Boolean.Iteration.boolean_orderedBudget_le (n m q : ℕ) : signature.orderedBudget n m q ≤ (q + 1) * 5 ^ q * (n + q + 1) ^ (2 * q + m)

Constants, arbitrary fanout, and all designated outputs are counted in the De Morgan syntax budget.

theorem Cslib.Circuits.Boolean.Iteration.boolean_orderedBudget_le_pow (n m q h : ℕ) (hw : n + q + 1 ≤ 2 ^ h) : signature.orderedBudget n m q ≤ 2 ^ (3 * q + h * (2 * q + m + 1))

Binary logarithmic bound on the De Morgan syntax budget when the wire budget is at most 2 ^ h.

theorem Cslib.Circuits.Boolean.Iteration.square_le_exponential (k : ℕ) (hk : 64 ≤ k) : 128 * (k + 2) ^ 2 ≤ 2 ^ k

For k ≥ 64, 128 * (k + 2) ^ 2 ≤ 2 ^ k.

def Cslib.Circuits.Boolean.Iteration.lowerBudget (k : ℕ) : ℕ

Explicit exponential gate threshold 2 ^ k / (1024 * (k + 1)) for 2 k-bit modular counters.

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

The number of descriptions below lowerBudget k has binary logarithm strictly below 2 ^ k - 1 - k.

theorem Cslib.Circuits.Boolean.Iteration.lowerBudget_wire_bound (k : ℕ) (hk : 64 ≤ k) : k + k + lowerBudget k + 1 ≤ 2 ^ (k + 2)

The wire count for 2 k inputs and lowerBudget k gates fits in 2 ^ (k + 2).

theorem Cslib.Circuits.Boolean.Iteration.exists_hard_power_of_budget_lt {n : ℕ} (g : BitString n → BitString n) (q : ℕ) (large : signature.orderedBudget n n q < FunctionalGraph.maxTransientDepth g + FunctionalGraph.cyclePeriod g) : ∃ T < FunctionalGraph.maxTransientDepth g + FunctionalGraph.cyclePeriod g, ∀ (out : Circuit signature n n), out.Computes interpretation g^[T] → q < out.size

Counting step. If the ordered-syntax budget for q gates is smaller than the number of distinct powers maxTransientDepth g + cyclePeriod g, some power below maxTransientDepth g + cyclePeriod g has no circuit with at most q gates.

theorem Cslib.Circuits.Boolean.Iteration.exists_hard_power {n : ℕ} (g : BitString n → BitString n) (q h : ℕ) (hw : n + q + 1 ≤ 2 ^ h) (large : 2 ^ (3 * q + h * (2 * q + n + 1)) < FunctionalGraph.maxTransientDepth g + FunctionalGraph.cyclePeriod g) : ∃ T < FunctionalGraph.maxTransientDepth g + FunctionalGraph.cyclePeriod g, ∀ (out : Circuit signature n n), out.Computes interpretation g^[T] → q < out.size

An explicit exponent form of the counting step, via boolean_orderedBudget_le_pow.