Documentation

Complexitylib.Circuits.Shallow

Optimal shallow-circuit upper bounds for symmetric functions #

Theorem 1 of Victor Lecomte and Prasanna Ramakrishnan, Optimal Shallow Circuits for Majority, arXiv:2609.34029v1 (2026): for each fixed d ≥ 2, every symmetric function on n inputs has an unbounded-fan-in AND/OR circuit of depth at most d and size 2^{O(n^{1/(d-1)})}. The constant is uniform over all symmetric functions.

The witnesses are native Cslib.Circuits.Circuits. Gates have arbitrary fan-in, size counts AND/OR gates, and negations occur only at primary inputs. The construction is nonuniform. The integer-root bound also includes n = 0; the real-exponent bound is stated for n ≥ 1.

This formalizes the paper's upper bound. Håstad's matching lower bound is background to the optimality claim and is not reproved in this development. Majority accepts ties, following the paper's convention.

Reference #

theorem Complexity.Shallow.symmetric_upper_bound_nat (d : ℕ) (hd : 2 ≤ d) :
∃ (C : ℕ), ∀ (n : ℕ) (f : BitString n → Bool), Symmetric f → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.depth ≤ d ∧ c.size ≤ 2 ^ (C * ((d - 1).nthRoot n + 1)) ∧ InputNegationsOnly c

Lecomte--Ramakrishnan, Theorem 1, with an exact integer-root size bound, including empty input and explicit restriction of negations to primary inputs.

theorem Complexity.Shallow.symmetric_upper_bound (d : ℕ) (hd : 2 ≤ d) :
∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), Symmetric f → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.depth ≤ d ∧ ↑c.size ≤ 2 ^ (C * ↑n ^ (1 / ↑(d - 1))) ∧ InputNegationsOnly c

Lecomte--Ramakrishnan, Theorem 1. One constant for each depth bounds the size of circuits for every symmetric Boolean function.

theorem Complexity.Shallow.symmetric_depth_three :
∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), Symmetric f → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.depth ≤ 3 ∧ ↑c.size ≤ 2 ^ (C * √↑n) ∧ InputNegationsOnly c

Lecomte--Ramakrishnan, Theorem 2. Depth-three circuits for symmetric functions have size at most 2^(C * sqrt n), uniformly over the function.

theorem Complexity.Shallow.majority_upper_bound (d : ℕ) (hd : 2 ≤ d) :
∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => majority x) ∧ c.depth ≤ d ∧ ↑c.size ≤ 2 ^ (C * ↑n ^ (1 / ↑(d - 1))) ∧ InputNegationsOnly c

Majority has the paper's upper bound at every fixed depth at least two.