From top-down communication bounds to circuit size bounds

Generic glue shared by the parity and majority top-down lower bounds. A communication lower bound for rounds-message KW protocols whose per-message cost is at most ε * n^(1/(rounds-1)) yields

• a wire bound, via the totalFanIn-alphabet protocol of exists_roundProtocol;
• a gate bound 2^(ε * n^(1/(rounds-1))) < 2 * (n + g), via the 2 * (n + g)-alphabet protocol of exists_roundProtocol_of_gates;
• a superpolynomial gate bound for every fixed depth, because every polynomial is eventually below 2^(ε * n^r) for r > 0 (eventually_poly_le_two_rpow_internal).

theorem Complexity.Circuit.eventually_poly_le_two_rpow_internal {r ε : ℝ} (hr : 0 < r) (hε : 0 < ε) (k C : ℕ) : ∃ (n0 : ℕ), ∀ (n : ℕ), n0 ≤ n → ↑(2 * (n + (C * n ^ k + C))) ≤ 2 ^ (ε * ↑n ^ r)

Every polynomial bound of the shape 2 * (n + (C * n^k + C)) is eventually at most 2^(ε * n^r) when r and ε are positive.

theorem Complexity.Circuit.wire_lower_bound_of_communication_internal (f : (n : ℕ) → BitString n → Bool) (rounds : ℕ) (hcomm : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ {M : Type} [inst : Fintype M] [DecidableEq M] (m : ℝ), 0 ≤ m → ↑(Fintype.card M) ≤ 2 ^ m → m ≤ ε * ↑n ^ (↑(rounds - 1))⁻¹ → ∀ (P : KarchmerWigderson.RoundProtocol (Fin n) M rounds), ¬P.SolvesKW (f n)) : ∃ (ε : ℝ), 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 = f n x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < ↑c.totalFanIn

A top-down communication lower bound for a function family f gives the corresponding exponential lower bound on input-wire occurrences.

theorem Complexity.Circuit.gate_size_lower_bound_of_communication_internal (f : (n : ℕ) → BitString n → Bool) (rounds : ℕ) (hcomm : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ {M : Type} [inst : Fintype M] [DecidableEq M] (m : ℝ), 0 ≤ m → ↑(Fintype.card M) ≤ 2 ^ m → m ≤ ε * ↑n ^ (↑(rounds - 1))⁻¹ → ∀ (P : KarchmerWigderson.RoundProtocol (Fin n) M rounds), ¬P.SolvesKW (f n)) : ∃ (ε : ℝ), 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 = f n x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < 2 * (↑n + ↑g)

A top-down communication lower bound for a function family f gives an exponential lower bound on 2 * (n + g), where g is the number of internal gates.

theorem Complexity.Circuit.superpolynomial_gates_of_gate_size_internal (f : (n : ℕ) → BitString n → Bool) (hgate : ∀ (rounds : ℕ), 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 = f n x) → 2 ^ (ε * ↑n ^ (↑(rounds - 1))⁻¹) < 2 * (↑n + ↑g)) (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 = f n x) → C * n ^ k + C < g

If a function family satisfies the exponential gate bound at every depth rounds ≥ 2, then for every fixed depth and polynomial C * n^k + C, all sufficiently large bounded-depth circuits computing it have more than C * n^k + C internal gates.