Low-degree functions over ZMod 3 -- definitions

Smolensky's lower bound approximates circuits by low-degree polynomials over the field with three elements. This module avoids formal polynomials: it works with functions {0,1}^n → ZMod 3 directly, reading each input bit as 0 or 1 in ZMod 3. The monomial of a set S of coordinates is the function x ↦ ∏_{i ∈ S} x_i, and a function has degree at most D when it is a ZMod 3-linear combination of monomials of at most D coordinates. On Boolean inputs every polynomial function is multilinear, so this is the usual notion of degree for functions on the Boolean cube.

Main definitions

• Smolensky.bitVal — a bit read as 0 or 1 in ZMod 3
• Smolensky.monomial — the function x ↦ ∏_{i ∈ S} x_i
• Smolensky.lowDegree — the submodule of functions of degree at most D

def Complexity.Smolensky.bitVal (b : Bool) : ZMod 3

A bit read as 0 or 1 in ZMod 3.

Equations

• Complexity.Smolensky.bitVal b = if b = true then 1 else 0

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

The monomial of a set S of coordinates: the product of the selected input bits, read in ZMod 3. The empty monomial is the constant 1.

Equations

• Complexity.Smolensky.monomial S x = ∏ i ∈ S, Complexity.Smolensky.bitVal (x i)

def Complexity.Smolensky.lowDegree (n D : ℕ) : Submodule (ZMod 3) (BitString n → ZMod 3)

The functions {0,1}^n → ZMod 3 of degree at most D: the ZMod 3-linear span of the monomials of at most D coordinates.

Equations

• Complexity.Smolensky.lowDegree n D = Submodule.span (ZMod 3) (Complexity.Smolensky.monomial '' {S : Finset (Fin n) | S.card ≤ D})