Parity is hard to approximate by low-degree functions over ZMod 3

Write yᵢ = 1 + xᵢ ∈ {1, -1} ⊆ ZMod 3, so that ∏ᵢ yᵢ = (-1)^{|x|} is parity in ±1 form and every yᵢ² = 1. If a degree-D function Q agrees with ∏ᵢ yᵢ on a set G, then on G every y-monomial y_S with |S| > n/2 equals Q · y_{Sᶜ}, of degree at most D + n/2. Since the y-monomials span all functions, every function G → ZMod 3 is the restriction of a function of degree at most n/2 + D. Comparing cardinalities, 3^{|G|} is at most 3 to the number of monomials of at most n/2 + D coordinates.

def Complexity.Smolensky.signMonomial {n : ℕ} (S : Finset (Fin n)) (x : BitString n) : ZMod 3

The product of the ±1 variables yᵢ = 1 + xᵢ over S.

Equations

• Complexity.Smolensky.signMonomial S x = ∏ i ∈ S, (1 + Complexity.Smolensky.bitVal (x i))

def Complexity.Smolensky.signSpan (n H : ℕ) : Submodule (ZMod 3) (BitString n → ZMod 3)

The span of the ±1 monomials of at most H coordinates.

Equations

• Complexity.Smolensky.signSpan n H = Submodule.span (ZMod 3) (Complexity.Smolensky.signMonomial '' {S : Finset (Fin n) | S.card ≤ H})

theorem Complexity.Smolensky.signMonomial_mem_lowDegree {n : ℕ} (S : Finset (Fin n)) : signMonomial S ∈ lowDegree n S.card

theorem Complexity.Smolensky.one_add_bitVal_sq (b : Bool) : (1 + bitVal b) ^ 2 = 1

theorem Complexity.Smolensky.signMonomial_sq {n : ℕ} (S : Finset (Fin n)) (x : BitString n) : signMonomial S x ^ 2 = 1

theorem Complexity.Smolensky.signMonomial_mul_compl {n : ℕ} (S : Finset (Fin n)) (x : BitString n) : signMonomial S x * signMonomial Sᶜ x = signMonomial Finset.univ x

theorem Complexity.Smolensky.one_add_bitVal_mul (a b : Bool) : (1 + bitVal a) * (1 + bitVal b) = 1 + bitVal (a ^^ b)

theorem Complexity.Smolensky.signMonomial_univ {n : ℕ} (x : BitString n) : signMonomial Finset.univ x = 1 + bitVal (Schnorr.xorBool n x)

The product of all ±1 variables is parity in ±1 form.

theorem Complexity.Smolensky.mem_lowDegree_self {n : ℕ} (f : BitString n → ZMod 3) : f ∈ lowDegree n n

Every function on the cube has degree at most n.

theorem Complexity.Smolensky.signSpan_mono {n H K : ℕ} (hHK : H ≤ K) : signSpan n H ≤ signSpan n K

theorem Complexity.Smolensky.monomial_mem_signSpan {n : ℕ} (S : Finset (Fin n)) : monomial S ∈ signSpan n S.card

Each monomial expands into ±1 monomials of its subsets.

theorem Complexity.Smolensky.lowDegree_le_signSpan {n : ℕ} (H : ℕ) : lowDegree n H ≤ signSpan n H

theorem Complexity.Smolensky.exists_agree_of_parity {n D : ℕ} {Q : BitString n → ZMod 3} (hQ : Q ∈ lowDegree n D) (G : Finset (BitString n)) (hG : ∀ x ∈ G, Q x = signMonomial Finset.univ x) (f : BitString n → ZMod 3) : ∃ p ∈ lowDegree n (n / 2 + D), ∀ x ∈ G, p x = f x

If Q has degree at most D and agrees with the ±1 parity on G, every function agrees on G with a function of degree at most n / 2 + D.

theorem Complexity.Smolensky.card_le_of_forall_exists_agree {n H : ℕ} (G : Finset (BitString n)) (hG : ∀ (f : BitString n → ZMod 3), ∃ p ∈ lowDegree n H, ∀ x ∈ G, p x = f x) : G.card ≤ {S : Finset (Fin n) | S.card ≤ H}.card

If every function agrees on G with a function of degree at most H, then |G| is at most the number of monomials of at most H coordinates.

theorem Complexity.Smolensky.card_agree_xorBool_le_internal {n D : ℕ} {P : BitString n → ZMod 3} (hP : P ∈ lowDegree n D) : {x : BitString n | P x = bitVal (Schnorr.xorBool n x)}.card ≤ {S : Finset (Fin n) | S.card ≤ n / 2 + D}.card

Parity is hard to approximate. A function of degree at most D agrees with parity on at most as many inputs as there are monomials of at most n / 2 + D coordinates.