The wire and gate lower bounds in Korten's Theorem 3

Apply the checked communication bound to the protocol of a circuit. Taking the putative message cost to be the real threshold itself avoids rounding a logarithm: totalFanIn ≤ 2^m is exactly the needed alphabet-size bound. The same argument with the 2 * (n + g)-symbol protocol bounds the number g of internal gates, and the exponential gate bound at every depth gives a superpolynomial gate bound at each fixed depth.

Source: Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

theorem Complexity.Circuit.parity_wire_lower_bound_internal (rounds : ℕ) (hrounds : 2 ≤ rounds) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (n0 : ℕ), ∀ (n : ℕ), n0 ≤ n → ∀ [inst : NeZero n] (g : ℕ) (c : Circuit Basis.unboundedAndOr n 1 g), c.depth ≤ rounds → (∀ (x : BitString n), c.eval x 0 = Schnorr.xorBool n x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < ↑c.totalFanIn

theorem Complexity.Circuit.parity_gate_size_lower_bound_internal (rounds : ℕ) (hrounds : 2 ≤ rounds) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (n0 : ℕ), ∀ (n : ℕ), n0 ≤ n → ∀ [inst : NeZero n] (g : ℕ) (c : Circuit Basis.unboundedAndOr n 1 g), c.depth ≤ rounds → (∀ (x : BitString n), c.eval x 0 = Schnorr.xorBool n x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < 2 * (↑n + ↑g)

theorem Complexity.Circuit.parity_superpolynomial_gates_internal (rounds k C : ℕ) : ∃ (n0 : ℕ), ∀ (n : ℕ), n0 ≤ n → ∀ [inst : NeZero n] (g : ℕ) (c : Circuit Basis.unboundedAndOr n 1 g), c.depth ≤ rounds → (∀ (x : BitString n), c.eval x 0 = Schnorr.xorBool n x) → C * n ^ k + C < g