Smolensky's gate approximators

Over a commutative ring R of prime characteristic p, such as ZMod p or the fields of order p ^ k in which Smolensky works [Smo87], every gate of the AC⁰[p] basis has a polynomial approximator that multiplies degrees by at most (p - 1) ℓ:

• MOD_p of bits u₁, …, u_m is exactly (∑ uᵢ) ^ (p - 1), since the sum is the image of the count in the prime field ZMod p, where nonzero elements have (p - 1)-st power 1 (natCast_pow_eq_bitVal, modApprox);
• OR of u₁, …, u_m is approximated by 1 - ∏_{j < ℓ} (1 - (∑_{i ∈ T j} uᵢ) ^ (p - 1)) for a tuple T of ℓ sets of arguments (orApprox), and AND is its De Morgan dual;
• negation is exactly 1 - u.

For a nonzero Boolean vector, adding or removing a true coordinate changes the count of a set by one, so at most half of the sets have a count divisible by p, and at most a 2 ^ (-ℓ) fraction of the tuples err (card_orApprox_wrong_mul_le). Double counting over the inputs gives, for every gate and every way its arguments depend on the input, an approximator that errs on at most 2 ^ n / 2 ^ ℓ inputs (exists_gate_approx) [Raz87], [Smo87], Jukna, Chapter 12.

Main definitions

• Cslib.Circuits.Boolean.Smolensky.orApprox, Cslib.Circuits.Boolean.Smolensky.andApprox: the approximators of OR and AND for a tuple of sets of arguments.
• Cslib.Circuits.Boolean.Smolensky.modApprox: the MOD_p polynomial.

Main results

• Cslib.Circuits.Boolean.Smolensky.natCast_pow_eq_bitVal: Fermat's little theorem for counts in characteristic p.
• Cslib.Circuits.Boolean.Smolensky.exists_gate_approx: the gate approximators.

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
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Boolean.Smolensky.orApprox {R : Type u_1} [CommRing R] {m ℓ : ℕ} (p : ℕ) (T : Fin ℓ → Finset (Fin m)) (u : Fin m → R) : R

The OR approximator of characteristic p for a tuple T of ℓ sets of arguments.

def Cslib.Circuits.Boolean.Smolensky.andApprox {R : Type u_1} [CommRing R] {m ℓ : ℕ} (p : ℕ) (T : Fin ℓ → Finset (Fin m)) (u : Fin m → R) : R

The AND approximator, the De Morgan dual of orApprox.

def Cslib.Circuits.Boolean.Smolensky.modApprox {R : Type u_1} [CommRing R] {m : ℕ} (p : ℕ) (u : Fin m → R) : R

The MOD_p polynomial, exact in characteristic p.

theorem Cslib.Circuits.Boolean.Smolensky.orApprox_comp_mem {R : Type u_1} [CommRing R] {n m ℓ : ℕ} (p : ℕ) {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m → BitString n → R} (hv : ∀ (k : Fin m), v k ∈ BitString.lowDegree R (Fin n) D) : (fun (x : BitString n) => orApprox p T fun (k : Fin m) => v k x) ∈ BitString.lowDegree R (Fin n) (ℓ * ((p - 1) * D))

theorem Cslib.Circuits.Boolean.Smolensky.andApprox_comp_mem {R : Type u_1} [CommRing R] {n m ℓ : ℕ} (p : ℕ) {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m → BitString n → R} (hv : ∀ (k : Fin m), v k ∈ BitString.lowDegree R (Fin n) D) : (fun (x : BitString n) => andApprox p T fun (k : Fin m) => v k x) ∈ BitString.lowDegree R (Fin n) (ℓ * ((p - 1) * D))

theorem Cslib.Circuits.Boolean.Smolensky.modApprox_comp_mem {R : Type u_1} [CommRing R] {n m : ℕ} (p : ℕ) {D : ℕ} {v : Fin m → BitString n → R} (hv : ∀ (k : Fin m), v k ∈ BitString.lowDegree R (Fin n) D) : (fun (x : BitString n) => modApprox p fun (k : Fin m) => v k x) ∈ BitString.lowDegree R (Fin n) ((p - 1) * D)

Sums of bits

theorem Cslib.Circuits.Boolean.Smolensky.sum_bitVal {R : Type u_1} [CommRing R] {m : ℕ} (S : Finset (Fin m)) (u : Fin m → Bool) : ∑ i ∈ S, BitString.bitVal R (u i) = ↑{i ∈ S | u i = true}.card

A sum of bits is their count.

theorem Cslib.Circuits.Boolean.Smolensky.two_mul_card_sum_eq_zero_le {R : Type u_1} [CommRing R] {m : ℕ} [Nontrivial R] [DecidableEq R] (u : Fin m → Bool) {k : Fin m} (hk : u k = true) : 2 * {S : Finset (Fin m) | ∑ i ∈ S, BitString.bitVal R (u i) = 0}.card ≤ 2 ^ m

If some coordinate is true, at most half of the sets have a sum of bits equal to zero.

Exactness in characteristic p

theorem Cslib.Circuits.Boolean.Smolensky.orApprox_bitVal_of_forall_false {R : Type u_1} [CommRing R] {m ℓ p : ℕ} [Fact (Nat.Prime p)] (T : Fin ℓ → Finset (Fin m)) (u : Fin m → Bool) (hu : ∀ (i : Fin m), u i = false) : (orApprox p T fun (i : Fin m) => BitString.bitVal R (u i)) = 0

theorem Cslib.Circuits.Boolean.Smolensky.natCast_pow_eq_bitVal {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (c : ℕ) : ↑c ^ (p - 1) = BitString.bitVal R (decide (c % p ≠ 0))

The (p - 1)-st power of a count is whether the count is not divisible by p: in characteristic p the count is the image of its residue in ZMod p, where Fermat's little theorem applies.

theorem Cslib.Circuits.Boolean.Smolensky.natCast_pow_eq_one {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {c : ℕ} (hc : ↑c ≠ 0) : ↑c ^ (p - 1) = 1

In characteristic p, the (p - 1)-st power of a nonzero count is 1.

theorem Cslib.Circuits.Boolean.Smolensky.modApprox_bitVal {R : Type u_1} [CommRing R] {m p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (u : Fin m → Bool) : (modApprox p fun (i : Fin m) => BitString.bitVal R (u i)) = BitString.bitVal R (modGate p m u)

The MOD_p polynomial is exact on bits.

theorem Cslib.Circuits.Boolean.Smolensky.orApprox_bitVal_of_exists {R : Type u_1} [CommRing R] {m ℓ p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (T : Fin ℓ → Finset (Fin m)) (u : Fin m → Bool) (hT : ∃ (j : Fin ℓ), ∑ i ∈ T j, BitString.bitVal R (u i) ≠ 0) : (orApprox p T fun (i : Fin m) => BitString.bitVal R (u i)) = 1

Counting erring tuples

theorem Cslib.Circuits.Boolean.Smolensky.card_orApprox_wrong_mul_le {R : Type u_1} [CommRing R] {m ℓ p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [DecidableEq R] (u : Fin m → Bool) : {T : Fin ℓ → Finset (Fin m) | (orApprox p T fun (i : Fin m) => BitString.bitVal R (u i)) ≠ BitString.bitVal R (decide (∃ (j : Fin m), u j = true))}.card * 2 ^ ℓ ≤ (2 ^ m) ^ ℓ

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

theorem Cslib.Circuits.Boolean.Smolensky.exists_orApprox {R : Type u_1} [CommRing R] {n m ℓ p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [DecidableEq R] (u : BitString n → Fin m → Bool) : ∃ (T : Fin ℓ → Finset (Fin m)), {x : BitString n | (orApprox p T fun (i : Fin m) => BitString.bitVal R (u x i)) ≠ BitString.bitVal R (decide (∃ (j : Fin m), u x j = true))}.card * 2 ^ ℓ ≤ 2 ^ n

Averaging over the inputs. For arguments u x depending on the input, some tuple makes the OR approximator err on at most 2 ^ n / 2 ^ ℓ inputs.

theorem Cslib.Circuits.Boolean.Smolensky.exists_gate_approx {R : Type u_1} [CommRing R] {n ℓ p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [DecidableEq R] (hℓ : 1 ≤ ℓ) (op : Unbounded.extSignature.Op) (u : BitString n → Fin (Unbounded.extSignature.Arity op) → Bool) : ∃ (A : (Fin (Unbounded.extSignature.Arity op) → R) → R), (∀ (D : ℕ) (v : Fin (Unbounded.extSignature.Arity op) → BitString n → R), (∀ (k : Fin (Unbounded.extSignature.Arity op)), v k ∈ BitString.lowDegree R (Fin n) D) → (fun (x : BitString n) => A fun (k : Fin (Unbounded.extSignature.Arity op)) => v k x) ∈ BitString.lowDegree R (Fin n) ((p - 1) * ℓ * D)) ∧ {x : BitString n | (A fun (k : Fin (Unbounded.extSignature.Arity op)) => BitString.bitVal R (u x k)) ≠ BitString.bitVal R (Unbounded.extInterpretation (modGate p) op (u x))}.card * 2 ^ ℓ ≤ 2 ^ n

Gate approximators. Over a commutative ring R of characteristic p, for every operation of the AC⁰[p] basis and every way u its arguments depend on the input, some approximator multiplies degrees by at most (p - 1) ℓ and errs on at most 2 ^ n / 2 ^ ℓ inputs.