Top-down lower bounds for majority

The two adjacent Hamming layers surrounding the strict-majority threshold have logarithmic entropy deficit. Each point has at least half its coordinates leading to the other layer by a single-bit flip. This gives bilateral density limits at rate 16/n, and Korten's improved mirror-set adversary applies. The logarithmic initial deficit preserves the exponent 1/(d-1).

This extends the parity argument of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/. The majority predicate is the library's strict majority: ties are false, and both odd and even arities are covered. The circuit basis is unbounded AND/OR with free input negations.

Besides the wire bound majority_wire_lower_bound, the gate-count protocol of Circuit.exists_roundProtocol_of_gates gives majority_gate_size_lower_bound (2^(ε n^(1/(rounds-1))) < 2(n + g) for g internal gates) and majority_superpolynomial_gates: at every fixed depth, strict majority needs more than C * n^k + C internal gates for all sufficiently large n.

theorem Complexity.BooleanAnalysis.isDensityLimit_of_many_neighbors {n : ℕ} (hn : 16 ≤ n) (X : Finset (Fin n → Bool)) (x s : Fin n → Bool) (hs : n ≤ 2 * popCount s) (hneighbor : ∀ (i : Fin n), s i = true → (Function.update x i !x i) ∈ X) : IsDensityLimit X (16 / ↑n) 128 x

Many single-bit neighbors give a density limit at a sparse sampling rate. At least half the coordinates must flip the given point into X.

theorem Complexity.BooleanAnalysis.majority_layers_deficit {n : ℕ} (hn : 2 ≤ n) : ((weightLayer n (n / 2)).Nonempty ∧ uniformDeficit (weightLayer n (n / 2)) ≤ majorityDeficitBound n) ∧ (weightLayer n (n / 2 + 1)).Nonempty ∧ uniformDeficit (weightLayer n (n / 2 + 1)) ≤ majorityDeficitBound n

Both majority boundary layers are nonempty and have logarithmic entropy deficit.

theorem Complexity.BooleanAnalysis.majority_layers_limits {n : ℕ} (hn : 16 ≤ n) : (∀ x ∈ weightLayer n (n / 2), IsDensityLimit (weightLayer n (n / 2 + 1)) (16 / ↑n) (majorityDeficitBound n) x) ∧ ∀ y ∈ weightLayer n (n / 2 + 1), IsDensityLimit (weightLayer n (n / 2)) (16 / ↑n) (majorityDeficitBound n) y

The majority boundary layers satisfy bilateral density limits at rate 16/n.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_majority_finite {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

Explicit finite obstruction for strict-majority protocols with at most d+1 messages. The logarithmic initial deficit appears additively alongside the per-message cost.

theorem Complexity.KarchmerWigderson.majority_communication_lower_bound (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

For every fixed number of rounds at least two, strict majority requires per-message cost greater than epsilon*n^(1/(rounds-1)) for sufficiently large n. The constant and threshold depend only on the round bound.

theorem Complexity.Circuit.majority_wire_lower_bound (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

Every sufficiently large strict-majority circuit of depth at most rounds ≥ 2 has more than 2^(epsilon*n^(1/(rounds-1))) input-wire occurrences. Both odd and even input arities are covered, and per-input negations are free.

theorem Complexity.Circuit.majority_gate_size_lower_bound (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)

Every sufficiently large strict-majority circuit of depth at most rounds ≥ 2 with g internal gates satisfies 2^(epsilon*n^(1/(rounds-1))) < 2 * (n + g). The constant depends only on rounds.

theorem Complexity.Circuit.majority_superpolynomial_gates (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

For any fixed depth bound rounds and polynomial parameters k, C, all sufficiently large unbounded AND/OR circuits of depth at most rounds computing strict majority require more than C * n ^ k + C internal gates.