Smolensky's bound -- assembly

The approximation theorem and the hardness of parity give the finite counting inequality; the binomial estimates turn it into an explicit size bound; and a polynomial-versus-exponential comparison rules out polynomial-size, constant-depth AND/OR/MOD_3 families computing parity.

theorem Complexity.Smolensky.depth_eq_outputDepth_zero {n G : ℕ} [NeZero n] {B : Basis} (C : Circuit B n 1 G) : C.depth = C.outputDepth 0

theorem Complexity.Smolensky.one_le_depth {n G : ℕ} [NeZero n] {B : Basis} (C : Circuit B n 1 G) : 1 ≤ C.depth

theorem Complexity.Smolensky.parity_counting_bound_internal {n G : ℕ} [NeZero n] {d ℓ : ℕ} (C : Circuit (Basis.unboundedAndOrMod 3) n 1 G) (hcomputes : C.Computes (Schnorr.xorBool n)) (hdepth : C.depth ≤ d) (hℓ : 1 ≤ ℓ) : 2 ^ ℓ * 2 ^ n ≤ 2 ^ ℓ * {S : Finset (Fin n) | S.card ≤ n / 2 + (2 * ℓ) ^ d}.card + C.size * 2 ^ n

The finite counting form of the Razborov–Smolensky bound.

theorem Complexity.Smolensky.hundred_mul_sq_le {n d ℓ : ℕ} (hd : 1 ≤ d) (hℓ : 1 ≤ ℓ) (hn : (40 * ℓ) ^ (2 * d) ≤ n) : 100 * ((2 * ℓ) ^ d + 1) ^ 2 ≤ n + 1

The arithmetic step: (40ℓ)^{2d} ≤ n gives 100 ((2ℓ)^d + 1)² ≤ n + 1.

theorem Complexity.Smolensky.two_mul_two_pow_le_size_internal {n G : ℕ} [NeZero n] {d ℓ : ℕ} (C : Circuit (Basis.unboundedAndOrMod 3) n 1 G) (hcomputes : C.Computes (Schnorr.xorBool n)) (hdepth : C.depth ≤ d) (hn : (40 * ℓ) ^ (2 * d) ≤ n) : 2 * 2 ^ ℓ ≤ 5 * C.size

The explicit Razborov–Smolensky size bound.

theorem Complexity.Smolensky.exists_eval_lt_two_pow (q : Polynomial ℕ) : ∃ (ℓ : ℕ), 1 ≤ ℓ ∧ Polynomial.eval ℓ q < 2 ^ ℓ

A natural-coefficient polynomial is eventually below 2^ℓ.

theorem Complexity.Smolensky.xorBool_not_mem_AC0Mod_three_internal : Schnorr.xorBool ∉ AC0Mod 3

Parity is not in AC0[3].