Low-degree functions over ZMod 3 -- degree arithmetic

Monomials multiply by union of their coordinate sets, since every bit is idempotent in ZMod 3. Hence degrees add under multiplication, and the low-degree submodules are closed under the operations used by Smolensky's gate approximators: constants, sums, differences, powers, and finite products.

theorem Complexity.Smolensky.bitVal_true : bitVal true = 1

theorem Complexity.Smolensky.bitVal_false : bitVal false = 0

theorem Complexity.Smolensky.bitVal_not (b : Bool) : (bitVal !b) = 1 - bitVal b

theorem Complexity.Smolensky.bitVal_xor (a b : Bool) : bitVal (a ^^ b) = if a = true then 1 - bitVal b else bitVal b

theorem Complexity.Smolensky.monomial_apply_eq_ite {n : ℕ} (S : Finset (Fin n)) (x : BitString n) : monomial S x = if ∀ i ∈ S, x i = true then 1 else 0

theorem Complexity.Smolensky.monomial_mul {n : ℕ} (S T : Finset (Fin n)) : monomial S * monomial T = monomial (S ∪ T)

theorem Complexity.Smolensky.monomial_empty {n : ℕ} : monomial ∅ = 1

theorem Complexity.Smolensky.monomial_singleton {n : ℕ} (i : Fin n) : monomial {i} = fun (x : BitString n) => bitVal (x i)

theorem Complexity.Smolensky.monomial_mem_lowDegree {n : ℕ} {S : Finset (Fin n)} {D : ℕ} (hS : S.card ≤ D) : monomial S ∈ lowDegree n D

theorem Complexity.Smolensky.lowDegree_mono {n D E : ℕ} (hDE : D ≤ E) : lowDegree n D ≤ lowDegree n E

theorem Complexity.Smolensky.mem_lowDegree_of_le {n D E : ℕ} {f : BitString n → ZMod 3} (hf : f ∈ lowDegree n D) (hDE : D ≤ E) : f ∈ lowDegree n E

theorem Complexity.Smolensky.one_mem_lowDegree {n : ℕ} (D : ℕ) : 1 ∈ lowDegree n D

theorem Complexity.Smolensky.const_mem_lowDegree {n : ℕ} (D : ℕ) (c : ZMod 3) : (fun (x : BitString n) => c) ∈ lowDegree n D

theorem Complexity.Smolensky.bitVal_mem_lowDegree {n : ℕ} (i : Fin n) : (fun (x : BitString n) => bitVal (x i)) ∈ lowDegree n 1

theorem Complexity.Smolensky.lowDegree_mul_le {n : ℕ} (a b : ℕ) : lowDegree n a * lowDegree n b ≤ lowDegree n (a + b)

theorem Complexity.Smolensky.mul_mem_lowDegree {n a b : ℕ} {f g : BitString n → ZMod 3} (hf : f ∈ lowDegree n a) (hg : g ∈ lowDegree n b) : f * g ∈ lowDegree n (a + b)

theorem Complexity.Smolensky.pow_mem_lowDegree {n a : ℕ} {f : BitString n → ZMod 3} (hf : f ∈ lowDegree n a) (k : ℕ) : f ^ k ∈ lowDegree n (k * a)

theorem Complexity.Smolensky.prod_mem_lowDegree {n : ℕ} {ι : Type u_1} (s : Finset ι) {a : ℕ} (f : ι → BitString n → ZMod 3) (hf : ∀ i ∈ s, f i ∈ lowDegree n a) : ∏ i ∈ s, f i ∈ lowDegree n (s.card * a)

theorem Complexity.Smolensky.sum_mem_lowDegree {n : ℕ} {ι : Type u_1} (s : Finset ι) {a : ℕ} (f : ι → BitString n → ZMod 3) (hf : ∀ i ∈ s, f i ∈ lowDegree n a) : ∑ i ∈ s, f i ∈ lowDegree n a

theorem Complexity.Smolensky.one_sub_mem_lowDegree {n a : ℕ} {f : BitString n → ZMod 3} (hf : f ∈ lowDegree n a) : 1 - f ∈ lowDegree n a