Parity initialization and the top-down communication bound

Flipping one free coordinate pairs the two parity classes in every nonempty fiber, giving density exactly 1/2. A rate-4/n mask is nonempty with probability at least 3/4. Both parity classes therefore satisfy the initial limit condition, with deficit one. Apply the bilateral density adversary and its checked parameter bound to obtain the communication part of Theorem 3.

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

theorem Complexity.BooleanAnalysis.expect_half_of_flip_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (hf : ∀ (x : ι → Bool), f (Function.update x i !x i) = !f x) (b : Bool) : (Finset.univ.expect fun (x : ι → Bool) => if f x = b then 1 else 0) = 1 / 2

theorem Complexity.BooleanAnalysis.coordinateDensity_half_of_flip_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (hf : ∀ (x : ι → Bool) (i : ι), f (Function.update x i !x i) = !f x) (P x : ι → Bool) (b : Bool) (i : ι) (hi : P i = true) : coordinateDensity {z : ι → Bool | f z = b} P x = 1 / 2

theorem Complexity.BooleanAnalysis.parity_initial_internal {n : ℕ} (hn : 0 < n) (b : Bool) : {x : Fin n → Bool | Schnorr.xorBool n x = b}.Nonempty ∧ uniformDeficit {x : Fin n → Bool | Schnorr.xorBool n x = b} ≤ 1

theorem Complexity.BooleanAnalysis.parity_isDensityLimit_internal {n : ℕ} {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hsmall : (1 - p) ^ n ≤ 1 / 4) (b : Bool) (x : Fin n → Bool) : IsDensityLimit {z : Fin n → Bool | Schnorr.xorBool n z = b} p 1 x

theorem Complexity.BooleanAnalysis.parity_isDensityLimit_four_div_internal {n : ℕ} (hn : 4 ≤ n) (b : Bool) (x : Fin n → Bool) : IsDensityLimit {z : Fin n → Bool | Schnorr.xorBool n z = b} (4 / ↑n) 1 x

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_parity_finite_raw_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 : 16 * (32768 * 194 ^ d * (m + 1)) ^ d ≤ ↑n) : ¬P.Solves {x : Fin n → Bool | Schnorr.xorBool n x = false} {y : Fin n → Bool | Schnorr.xorBool n y = true}

theorem Complexity.KarchmerWigderson.RoundProtocol.not_solves_parity_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 : 16 * (32768 * 194 ^ d * (m + 1)) ^ d ≤ ↑n) : ¬P.SolvesKW (Schnorr.xorBool n)

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