Korten's communication lower bound for parity

The two parity classes of n bits have deficit one, and every nonempty fiber of either is half full, since flipping a free coordinate exchanges them; a mask of rate 4 / n is nonempty with probability at least 3 / 4, so each class consists of (4 / n, 1)-limits of the other. Korten's adversary then shows that no protocol with d + 1 messages of m bits solves the Karchmer–Wigderson game of parity once 16 (32768 · 194 ^ d (m + 1)) ^ d ≤ n (RoundProtocol.not_solvesKW_parity), so protocols with d messages need Ω(n ^ (1 / (d - 1))) bits Korten, Theorem 3 (not_solvesKW_parity).

Main results

• Cslib.Communication.RoundProtocol.not_solvesKW_parity: the bound with explicit constants.
• Cslib.Communication.not_solvesKW_parity: Korten's lower bound.

References

• O. Korten, Top-Down Lower Bounds for All Depths

theorem Cslib.Communication.parity_isDensityLimit {n : ℕ} {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hsmall : (1 - p) ^ n ≤ 1 / 4) (b : Bool) (x : Fin n → Bool) : BitString.IsDensityLimit {z : Fin n → Bool | parity n z = b} p 1 x

The points are density limits of a parity class when masks are nonempty with probability at least 3 / 4.

theorem Cslib.Communication.RoundProtocol.not_solvesKW_parity {M : Type u_1} [Fintype M] {n d : ℕ} (P : KWRoundProtocol (Fin n) M (d + 1)) {m : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hsize : 16 * (32768 * 194 ^ d * (m + 1)) ^ d ≤ ↑n) : ¬SolvesKW P (parity n)

Korten's bound for parity, with explicit constants: no protocol with d + 1 messages of at most m bits solves the Karchmer–Wigderson game of parity on n bits when 16 (32768 · 194 ^ d (m + 1)) ^ d ≤ n.

theorem Cslib.Communication.not_solvesKW_parity (rounds : ℕ) (hrounds : 2 ≤ rounds) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ {M : Type u} [inst : Fintype M], ↑(Fintype.card M) ≤ 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) → ∀ (P : KWRoundProtocol (Fin n) M rounds), ¬RoundProtocol.SolvesKW P (parity n)

Korten's communication lower bound for parity Korten, Theorem 3: for every d ≥ 2 there is ε > 0 such that, for all large n, no protocol with d messages from an alphabet of at most 2 ^ (ε n ^ (1 / (d - 1))) letters solves the Karchmer–Wigderson game of parity on n bits.