Top-down lower bounds for circuits of constant depth

A circuit over the unbounded fan-in basis gives a Karchmer–Wigderson protocol in which the players walk down from the output Korten, Section 1.1: at a conjunction the player whose input makes it false names an argument wire false on that input, at a disjunction the player whose input makes it true names an argument true on it, a negation exchanges the roles without a message, and at an input the two inputs differ (Unbounded.kwProtocol, Unbounded.kwProtocol_solves). The messages are wires, so a circuit of AND/OR depth d (its depth with negations free, Circuit.depthWith Unbounded.andOrCost) with g gates on n inputs gives a protocol with d messages from an alphabet of size n + g.

Korten's theorem Korten, Theorem 3 bounds such protocols for parity, so for every d ≥ 2 there is ε > 0 such that circuits of AND/OR depth d for the parity of n bits have n + g > 2 ^ (ε n ^ (1 / (d - 1))) for all large n (Unbounded.two_rpow_lt_add_size_of_computes_parity). The exponent 1 / (d - 1) improves on the 1 / (d + 1) of Unbounded.two_pow_le_size_of_computes_parity, and is optimal, since parity has circuits of AND/OR depth d with 2 ^ O(n ^ (1 / (d - 1))) gates [Has86]. Negations are free in this depth, so the bound also holds for Circuit.depth, which counts them (Circuit.depthWith_le_depth). The same bound holds for strict majority, and for majority, whose protocols give protocols for strict majority by negating the inputs and exchanging the players (Unbounded.two_rpow_lt_add_size_of_computes_majority), extending Korten's theorem. At every fixed depth, both need more than n ^ k gates for large n (Unbounded.pow_lt_size_of_computes_parity, Unbounded.pow_lt_size_of_computes_majority).

Main definitions

• Cslib.Circuits.Boolean.Unbounded.kwProtocol: the Karchmer–Wigderson protocol of a wire.

Main results

• Cslib.Circuits.Boolean.Unbounded.kwProtocol_solves: it solves the game of the wire.
• Cslib.Circuits.Boolean.Unbounded.two_rpow_lt_add_size_of_computes_parity: Korten's theorem.
• Cslib.Circuits.Boolean.Unbounded.two_rpow_lt_add_size_of_computes_majority: the same for majority, extending Korten's theorem.
• Cslib.Circuits.Boolean.Unbounded.pow_lt_size_of_computes_parity, Cslib.Circuits.Boolean.Unbounded.pow_lt_size_of_computes_majority: at every fixed depth, parity and majority need more than n ^ k gates for large n.

References

• O. Korten, Top-Down Lower Bounds for All Depths
• J. Håstad, Almost Optimal Lower Bounds for Small Depth Circuits

def Cslib.Circuits.Boolean.Unbounded.argWith {n g : ℕ} (p : Program signature n g) (k : Fin g) (b : Bool) (x : BitString n) : Wire n g

The first argument wire of gate k that is b on the input x, if there is one.

theorem Cslib.Circuits.Boolean.Unbounded.argWith_spec {n g : ℕ} {p : Program signature n g} {k : Fin g} {b : Bool} {x : BitString n} (h : ∃ (a : Fin (signature.Arity (p.lines k).op)), p.trace interpretation x ((p.lines k).wires a) = b) : ∃ (a : Fin (signature.Arity (p.lines k).op)), argWith p k b x = (p.lines k).wires a ∧ p.trace interpretation x ((p.lines k).wires a) = b

def Cslib.Circuits.Boolean.Unbounded.firstArg {n g : ℕ} (p : Program signature n g) (i₀ : Fin n) (k : Fin g) : Wire n g

The first argument wire of gate k, or the input i₀ if it has none.

theorem Cslib.Circuits.Boolean.Unbounded.wireDepths_firstArg_lt {n g : ℕ} (p : Program signature n g) (i₀ : Fin n) (k : Fin g) : p.wireDepths (firstArg p i₀ k) < p.depths k

theorem Cslib.Circuits.Boolean.Unbounded.firstArg_of_op_eq_not {n g : ℕ} {p : Program signature n g} {k : Fin g} (i₀ : Fin n) (h : (p.lines k).op = Op.not) : firstArg p i₀ k = (p.lines k).wires ⟨0, ⋯⟩

@[irreducible]

def Cslib.Circuits.Boolean.Unbounded.kwProtocol {n g : ℕ} (p : Program signature n g) (i₀ : Fin n) (d : ℕ) (w : Wire n g) (s : Bool) : Communication.KWRoundProtocol (Fin n) (Wire n g) d

The Karchmer–Wigderson protocol of the wire w with at most d messages: Alice holds an input where w is s, Bob one where it is !s. At a conjunction the player whose input makes it false names an argument false there, at a disjunction the player whose input makes it true names an argument true there, and a negation exchanges the roles. The default coordinate i₀ is the output when the budget runs out.

theorem Cslib.Circuits.Boolean.Unbounded.kwProtocol_solves {n g : ℕ} (p : Program signature n g) (i₀ : Fin n) (d : ℕ) (w : Wire n g) (s : Bool) (hw : Program.wireDepthsWith andOrCost p w ≤ d) (x y : BitString n) (hx : p.trace interpretation x w = s) (hy : p.trace interpretation y w = !s) : x (Communication.RoundProtocol.run (kwProtocol p i₀ d w s) x y) ≠ y (Communication.RoundProtocol.run (kwProtocol p i₀ d w s) x y)

The protocol of a wire solves its game: if the wire w has AND/OR depth at most d, Alice's input makes it s and Bob's makes it !s, the two inputs differ at the named coordinate.

theorem Cslib.Circuits.Boolean.Unbounded.exists_roundProtocol_of_computes {n : ℕ} {C : Circuit signature n 1} {f : BitString n → Bool} (hC : C.Computes interpretation (single f)) (i₀ : Fin n) {d : ℕ} (hd : Circuit.depthWith andOrCost C ≤ d) : ∃ (P : Communication.KWRoundProtocol (Fin n) (Wire n C.size) d), Communication.RoundProtocol.SolvesKW P f

A circuit gives a protocol: a circuit of AND/OR depth at most d computing f on n ≥ 1 inputs gives a Karchmer–Wigderson protocol for f with at most d messages from its wires.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_lt_add_size_of_computes_parity {d : ℕ} (hd : 2 ≤ d) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit signature n 1), C.Computes interpretation (single (parity n)) → Circuit.depthWith andOrCost C ≤ d → 2 ^ (ε * ↑n ^ (↑(d - 1))⁻¹) < ↑n + ↑C.size

Korten's theorem Korten, Theorem 3: for every depth d ≥ 2 there is ε > 0 such that, for all large n, a circuit over the unbounded fan-in basis of AND/OR depth at most d computing the parity of n bits has n + g > 2 ^ (ε n ^ (1 / (d - 1))), where g is its number of gates.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_lt_add_size_of_computes_strictMajority {d : ℕ} (hd : 2 ≤ d) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit signature n 1), C.Computes interpretation (single (strictMajority n)) → Circuit.depthWith andOrCost C ≤ d → 2 ^ (ε * ↑n ^ (↑(d - 1))⁻¹) < ↑n + ↑C.size

Korten's bound for strict majority, extending [Kor26]: the bound of two_rpow_lt_add_size_of_computes_parity holds for strict majority.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_lt_add_size_of_computes_majority {d : ℕ} (hd : 2 ≤ d) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit signature n 1), C.Computes interpretation (single (majority n)) → Circuit.depthWith andOrCost C ≤ d → 2 ^ (ε * ↑n ^ (↑(d - 1))⁻¹) < ↑n + ↑C.size

Korten's bound for majority, extending [Kor26]: the bound of two_rpow_lt_add_size_of_computes_parity holds for majority. A protocol for majority gives one for strict majority by negating the inputs and exchanging the players.

theorem Cslib.Circuits.Boolean.Unbounded.pow_lt_size_of_two_rpow_lt {σ : Signature} {Q : (n : ℕ) → Circuit σ n 1 → Prop} {r ε : ℝ} (hr : 0 < r) (hε : 0 < ε) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Circuit σ n 1), Q n C → 2 ^ (ε * ↑n ^ r) < ↑n + ↑C.size) (k : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Circuit σ n 1), Q n C → n ^ k < C.size

Bounds n + g > 2 ^ (ε n ^ r) with r, ε > 0 on the circuits satisfying Q give more than n ^ k gates for large n.

theorem Cslib.Circuits.Boolean.Unbounded.pow_lt_size_of_computes_parity (d k : ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit signature n 1), C.Computes interpretation (single (parity n)) → Circuit.depthWith andOrCost C ≤ d → n ^ k < C.size

Parity is not in AC⁰, superpolynomially [Kor26]: for every depth d and exponent k, circuits over the unbounded fan-in basis of AND/OR depth at most d computing the parity of n bits have more than n ^ k gates for all large n.

theorem Cslib.Circuits.Boolean.Unbounded.pow_lt_size_of_computes_majority (d k : ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit signature n 1), C.Computes interpretation (single (majority n)) → Circuit.depthWith andOrCost C ≤ d → n ^ k < C.size

Majority is not in AC⁰, superpolynomially, extending [Kor26]: for every depth d and exponent k, circuits over the unbounded fan-in basis of AND/OR depth at most d computing the majority of n bits have more than n ^ k gates for all large n.