Smolensky's gate approximators

Each gate of the AND/OR/MOD_3 basis gets a polynomial approximator over ZMod 3 that multiplies degrees by at most 2ℓ:

• MOD_3 of u₁, …, u_m is exactly (∑ uᵢ)², because a nonzero element of ZMod 3 squares to 1;
• OR of u₁, …, u_m is approximated by 1 - ∏_{j < ℓ} (1 - (∑_{i ∈ T j} uᵢ)²) for a tuple T of ℓ subsets of the inputs;
• AND is the De Morgan dual of OR.

For a nonzero Boolean vector, pairing each subset with its symmetric difference with a true coordinate shows that at most half of all subsets have zero sum, so at most a 2^{-ℓ} fraction of the tuples err. Averaging over all inputs by exact double counting yields one tuple that errs on at most 2^{n-ℓ} inputs.

Semantics of the basis operations

theorem Complexity.Smolensky.or_eval_eq_true_iff (k : ℕ) (inputs : Fin k → Bool) : AndOrOp.or.eval k inputs = true ↔ ∃ (index : Fin k), inputs index = true

theorem Complexity.Smolensky.and_eval_eq_true_iff (k : ℕ) (inputs : Fin k → Bool) : AndOrOp.and.eval k inputs = true ↔ ∀ (index : Fin k), inputs index = true

theorem Complexity.Smolensky.and_eval_eq_not_or (k : ℕ) (inputs : Fin k → Bool) : AndOrOp.and.eval k inputs = !AndOrOp.or.eval k fun (index : Fin k) => !inputs index

theorem Complexity.Smolensky.sum_bitVal_eq_countP {m : ℕ} (inputs : Fin m → Bool) : ∑ i : Fin m, bitVal (inputs i) = ↑(Fin.countP inputs)

theorem Complexity.Smolensky.natCast_sq_eq_bitVal (c : ℕ) : ↑c ^ 2 = bitVal (decide (c % 3 ≠ 0))

theorem Complexity.Smolensky.sq_eq_one_of_ne_zero (a : ZMod 3) : a ≠ 0 → a ^ 2 = 1

The approximators

def Complexity.Smolensky.orApprox {m ℓ : ℕ} (T : Fin ℓ → Finset (Fin m)) (u : Fin m → ZMod 3) : ZMod 3

The OR approximator for a tuple T of ℓ subsets of the inputs.

Equations

• Complexity.Smolensky.orApprox T u = 1 - ∏ j : Fin ℓ, (1 - (∑ i ∈ T j, u i) ^ 2)

def Complexity.Smolensky.andApprox {m ℓ : ℕ} (T : Fin ℓ → Finset (Fin m)) (u : Fin m → ZMod 3) : ZMod 3

The AND approximator, the De Morgan dual of orApprox.

Equations

• Complexity.Smolensky.andApprox T u = 1 - Complexity.Smolensky.orApprox T fun (i : Fin m) => 1 - u i

def Complexity.Smolensky.modApprox {m : ℕ} (u : Fin m → ZMod 3) : ZMod 3

The exact MOD_3 polynomial.

Equations

• Complexity.Smolensky.modApprox u = (∑ i : Fin m, u i) ^ 2

theorem Complexity.Smolensky.orApprox_comp_mem {n m ℓ D : ℕ} (T : Fin ℓ → Finset (Fin m)) (v : Fin m → BitString n → ZMod 3) (hv : ∀ (k : Fin m), v k ∈ lowDegree n D) : (fun (x : BitString n) => orApprox T fun (k : Fin m) => v k x) ∈ lowDegree n (ℓ * (2 * D))

theorem Complexity.Smolensky.andApprox_comp_mem {n m ℓ D : ℕ} (T : Fin ℓ → Finset (Fin m)) (v : Fin m → BitString n → ZMod 3) (hv : ∀ (k : Fin m), v k ∈ lowDegree n D) : (fun (x : BitString n) => andApprox T fun (k : Fin m) => v k x) ∈ lowDegree n (ℓ * (2 * D))

theorem Complexity.Smolensky.modApprox_comp_mem {n m D : ℕ} (v : Fin m → BitString n → ZMod 3) (hv : ∀ (k : Fin m), v k ∈ lowDegree n D) : (fun (x : BitString n) => modApprox fun (k : Fin m) => v k x) ∈ lowDegree n (2 * D)

Counting erring tuples

theorem Complexity.Smolensky.two_mul_card_sum_eq_zero_le {m : ℕ} (u : Fin m → Bool) {k : Fin m} (hk : u k = true) : 2 * {S : Finset (Fin m) | ∑ i ∈ S, bitVal (u i) = 0}.card ≤ 2 ^ m

If some coordinate is true, at most half of all subsets have zero sum.

theorem Complexity.Smolensky.orApprox_bitVal_of_exists {m ℓ : ℕ} (T : Fin ℓ → Finset (Fin m)) (u : Fin m → Bool) (hT : ∃ (j : Fin ℓ), ∑ i ∈ T j, bitVal (u i) ≠ 0) : (orApprox T fun (i : Fin m) => bitVal (u i)) = 1

theorem Complexity.Smolensky.orApprox_bitVal_of_forall_false {m ℓ : ℕ} (T : Fin ℓ → Finset (Fin m)) (u : Fin m → Bool) (hu : ∀ (i : Fin m), u i = false) : (orApprox T fun (i : Fin m) => bitVal (u i)) = 0

theorem Complexity.Smolensky.card_orApprox_wrong_mul_le {m ℓ : ℕ} (u : Fin m → Bool) : {T : Fin ℓ → Finset (Fin m) | (orApprox T fun (i : Fin m) => bitVal (u i)) ≠ bitVal (AndOrOp.or.eval m u)}.card * 2 ^ ℓ ≤ (2 ^ m) ^ ℓ

At most a 2^{-ℓ} fraction of the tuples make the OR approximator err on a fixed Boolean vector.

theorem Complexity.Smolensky.exists_orApprox {n m ℓ : ℕ} (u : BitString n → BitString m) : ∃ (T : Fin ℓ → Finset (Fin m)), {x : BitString n | (orApprox T fun (i : Fin m) => bitVal (u x i)) ≠ bitVal (AndOrOp.or.eval m (u x))}.card * 2 ^ ℓ ≤ 2 ^ n

Averaging: some tuple makes the OR approximator err on at most 2^n / 2^ℓ of the inputs x, evaluated on the true input vector u x.

theorem Complexity.Smolensky.exists_gate_approx {n m ℓ : ℕ} (hℓ : 1 ≤ ℓ) (op : AndOrModOp) (u : BitString n → BitString m) : ∃ (A : (Fin m → ZMod 3) → ZMod 3), (∀ (D : ℕ) (v : Fin m → BitString n → ZMod 3), (∀ (k : Fin m), v k ∈ lowDegree n D) → (fun (x : BitString n) => A fun (k : Fin m) => v k x) ∈ lowDegree n (2 * ℓ * D)) ∧ {x : BitString n | (A fun (k : Fin m) => bitVal (u x k)) ≠ bitVal (AndOrModOp.eval 3 op m (u x))}.card * 2 ^ ℓ ≤ 2 ^ n

A gate approximator for every operation of the AND/OR/MOD_3 basis: it multiplies degrees by at most 2ℓ and errs on at most 2^n / 2^ℓ inputs, when evaluated on the gate's true input vector u x.