The Razborov–Smolensky lower bound

Parity is not in AC⁰[p] for every odd prime p (parity_notMem_AC0Mod): constant-depth, polynomial-size circuits of negations, unbounded fan-in conjunctions and disjunctions, and MOD_p gates do not compute parity [Raz87], [Smo87]. The finite form is a size–depth tradeoff (two_mul_two_pow_le_size_of_computes_parity): a circuit of depth d computing the parity of n bits has size at least 2 ^ ℓ · 2 / 5 whenever 100 (((p - 1) ℓ) ^ d + 1)² ≤ n + 1, so size 2 ^ Ω(n ^ (1 / (2 d))) for fixed d and p.

The circuit agrees with a function of degree at most ((p - 1) ℓ) ^ d over ZMod p (or any commutative ring of characteristic p) on all but size · 2 ^ n / 2 ^ ℓ inputs (exists_lowDegree_approx), while such a function agrees with parity on at most 6 / 10 of the inputs (BitString.card_agree_parity_le, ten_mul_card_filter_card_le_le).

Main results

• Cslib.Circuits.Boolean.Smolensky.two_mul_two_pow_le_size_of_computes_parity: the tradeoff.
• Cslib.Circuits.Boolean.Smolensky.parity_notMem_AC0Mod: parity is not in AC⁰[p].

References

• A. A. Razborov, Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

@[instance_reducible]

def Cslib.Circuits.Boolean.Smolensky.invertibleTwo {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Invertible 2

2 is invertible in ZMod p for an odd prime p.

theorem Cslib.Circuits.Boolean.Smolensky.two_mul_two_pow_le_size_of_computes_parity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hp2 : p ≠ 2) {C : Circuit Unbounded.extSignature n 1} (hC : C.Computes (Unbounded.extInterpretation (modGate p)) (single (parity n))) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hn : 100 * (((p - 1) * ℓ) ^ C.depth + 1) ^ 2 ≤ n + 1) : 2 * 2 ^ ℓ ≤ 5 * C.size

The Razborov–Smolensky size–depth tradeoff. A circuit of the AC⁰[p] basis of depth d computing the parity of n bits, for an odd prime p, has size at least 2 ^ ℓ · 2 / 5 whenever 100 (((p - 1) ℓ) ^ d + 1)² ≤ n + 1.

theorem Cslib.Circuits.Boolean.Smolensky.parity_notMem_AC0Mod {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Language.ofSlices parity ∉ AC0Mod p

Parity is not in AC⁰[p] for an odd prime p (Razborov–Smolensky).