Korten's top-down communication adversary

The improved mirror set maintains a density rectangle through arbitrary bounded-alphabet messages. The speaker may depend on the transcript. Early termination is ruled out by the absence of a fixed separating coordinate.

The finite bound with bilateral initial limits uses only d mirror steps for a protocol with at most d+1 messages. Parity initialization then proves the communication lower bound and its exponential wire corollary in Theorem 3 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

The gate-count protocol of Circuit.exists_roundProtocol_of_gates turns the same communication bound into parity_gate_size_lower_bound (2^(ε n^(1/(rounds-1))) < 2(n + g) for g internal gates) and hence parity_superpolynomial_gates: at every fixed depth, parity needs more than C * n^k + C internal gates for all sufficiently large n.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] [DecidableEq M] {d : ℕ} (P : RoundProtocol ι M d) {X Y : Finset (ι → Bool)} {m : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (k p : ℕ → ℝ) (hstep : ∀ i < d, 1 ≤ k i ∧ 194 * k i ≤ k (i + 1) ∧ 2 * k i + 2 + m ≤ k (i + 1) ∧ 32768 * k i * p i ≤ p (i + 1)) (hcap : ∀ i ≤ d, p i ≤ 1 / 4) (h : DensityRectangle X Y (p 0) (k 0)) : ¬P.Solves X Y

The density-rectangle adversary for any parameter sequences satisfying the one-message deficit and sampling-rate recurrences.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_bounded_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] [DecidableEq M] {d : ℕ} (P : RoundProtocol ι M d) {X Y : Finset (ι → Bool)} {m k p : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hk : 1 ≤ k) (hmk : m + 1 ≤ k) (hbudget : (32768 * 194 ^ d * k) ^ d * p ≤ 1 / 4) (h : DensityRectangle X Y p k) : ¬P.Solves X Y

Explicit finite specialization of the adversary for d rounds.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_bilateral_density_with_deficit {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] [DecidableEq M] {d : ℕ} (P : RoundProtocol ι M (d + 1)) {X Y : Finset (ι → Bool)} {m p k : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hk : 1 ≤ k) (hp : 0 < p) (hX : X.Nonempty) (hY : Y.Nonempty) (hdX : BooleanAnalysis.uniformDeficit X ≤ k) (hdY : BooleanAnalysis.uniformDeficit Y ≤ k) (hleft : ∀ x ∈ X, BooleanAnalysis.IsDensityLimit Y p k x) (hright : ∀ y ∈ Y, BooleanAnalysis.IsDensityLimit X p k y) (hbudget : (32768 * 194 ^ d * (m + k)) ^ d * p ≤ 1 / 4) : ¬P.Solves X Y

Bilateral initial limits save the first mirror step. This is the finite obstruction with an arbitrary initial deficit bound k ≥ 1.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_bilateral_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] [DecidableEq M] {d : ℕ} (P : RoundProtocol ι M (d + 1)) {X Y : Finset (ι → Bool)} {m p : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hp : 0 < p) (hX : X.Nonempty) (hY : Y.Nonempty) (hdX : BooleanAnalysis.uniformDeficit X ≤ 1) (hdY : BooleanAnalysis.uniformDeficit Y ≤ 1) (hleft : ∀ x ∈ X, BooleanAnalysis.IsDensityLimit Y p 1 x) (hright : ∀ y ∈ Y, BooleanAnalysis.IsDensityLimit X p 1 y) (hbudget : (32768 * 194 ^ d * (m + 1)) ^ d * p ≤ 1 / 4) : ¬P.Solves X Y

Bilateral initial limits save the first mirror step. This is the d-th-power obstruction for protocols with at most d+1 rounds.

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_parity_finite {M : Type u_2} [Fintype M] [DecidableEq M] {n d : ℕ} (P : RoundProtocol (Fin n) M (d + 1)) {m : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hsize : 16 * (32768 * 194 ^ d * (m + 1)) ^ d ≤ ↑n) : ¬P.SolvesKW (Schnorr.xorBool n)

Explicit finite obstruction for parity protocols with d+1 messages. The alphabet has at most 2^m symbols, and the displayed d-th-power condition is the checked finite form of the top-down bound.

theorem Complexity.KarchmerWigderson.parity_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 (Schnorr.xorBool n)

Communication part of Korten's Theorem 3: for every rounds ≥ 2, a positive constant depending only on rounds rules out all parity protocols whose per-message cost is at most epsilon*n^(1/(rounds-1)), for sufficiently large n. The quantifiers include every finite message alphabet.

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

Circuit part of Korten's Theorem 3. For every fixed depth at least two, all sufficiently large parity circuits over the unbounded De Morgan basis have more than 2^(epsilon*n^(1/(depth-1))) input-wire occurrences. The constant depends only on depth. Per-input negations are free.

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

Gate-count form of Korten's Theorem 3. For every fixed depth bound rounds ≥ 2, all sufficiently large parity circuits over the unbounded De Morgan basis with g internal gates satisfy 2^(epsilon*n^(1/(rounds-1))) < 2 * (n + g). The constant depends only on rounds.

theorem Complexity.Circuit.parity_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 = Schnorr.xorBool n 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 parity require more than C * n ^ k + C internal gates.