Top-down communication, wire, and gate lower bounds for majority

Initialize the generalized bilateral density adversary with the two majority boundary layers. Their logarithmic entropy loss is absorbed by the power-law budget. The circuit-to-protocol translations then give the wire bound, the exponential gate bound, and the superpolynomial gate bound at every fixed depth for unbounded De Morgan circuits with free input negations (via the shared glue in TopDown.Internal.GateBounds).

This extends the argument of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/. His Theorem 3 states the parity case; the majority initialization is proved here.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_majority_finite_internal {M : Type u_1} [Fintype M] [DecidableEq M] {n d : ℕ} (P : RoundProtocol (Fin n) M (d + 1)) {m : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hsize : 64 * (32768 * 194 ^ d * (m + BooleanAnalysis.majorityDeficitBound n)) ^ d ≤ ↑n) : ¬P.SolvesKW majority

theorem Complexity.KarchmerWigderson.majority_communication_lower_bound_internal (rounds : ℕ) (hrounds : 2 ≤ rounds) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ {M : Type u} [inst : Fintype M] [DecidableEq M] (m : ℝ), 0 ≤ m → ↑(Fintype.card M) ≤ 2 ^ m → m ≤ ε * ↑n ^ (↑(rounds - 1))⁻¹ → ∀ (P : RoundProtocol (Fin n) M rounds), ¬P.SolvesKW majority

theorem Complexity.Circuit.majority_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 = majority x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < ↑c.totalFanIn

theorem Complexity.Circuit.majority_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 = majority x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < 2 * (↑n + ↑g)

theorem Complexity.Circuit.majority_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 = majority x) → C * n ^ k + C < g