Smolensky's circuit approximation

Fix one gate approximator per gate of an AND/OR/MOD_3 circuit, chosen for the gate's true input vector. Composing them along the circuit gives, at every wire of depth e, a function of degree at most (2ℓ)^e. It is correct at every input on which every gate approximator is correct, so it errs on at most size · 2^n / 2^ℓ inputs.

theorem Complexity.Smolensky.gate_step {n W : ℕ} (wireValues : BitString n → BitString W) (gate : Gate (Basis.unboundedAndOrMod 3) W) (Bad : Finset (BitString n)) (A : (Fin gate.fanIn → ZMod 3) → ZMod 3) (ℓ e : ℕ) (hdeg : ∀ (D : ℕ) (v : Fin gate.fanIn → BitString n → ZMod 3), (∀ (k : Fin gate.fanIn), v k ∈ lowDegree n D) → (fun (x : BitString n) => A fun (k : Fin gate.fanIn) => v k x) ∈ lowDegree n (2 * ℓ * D)) (hbad : ∀ x ∉ Bad, (A fun (k : Fin gate.fanIn) => bitVal (gate.negated k ^^ wireValues x (gate.inputs k))) = bitVal (gate.eval (wireValues x))) (hinputs : ∀ (k : Fin gate.fanIn), ∃ P ∈ lowDegree n e, ∀ x ∉ Bad, P x = bitVal (wireValues x (gate.inputs k))) : ∃ P ∈ lowDegree n (2 * ℓ * e), ∀ x ∉ Bad, P x = bitVal (gate.eval (wireValues x))

One gate of the approximation: approximators of the gate's inputs and a gate approximator correct off Bad give an approximator of the gate.

theorem Complexity.Smolensky.exists_wire_approx {n G M : ℕ} [NeZero n] [NeZero M] (C : Circuit (Basis.unboundedAndOrMod 3) n M G) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (Bad : Finset (BitString n)) (A : (i : Fin G) → (Fin (C.gates i).fanIn → ZMod 3) → ZMod 3) (hdeg : ∀ (i : Fin G) (D : ℕ) (v : Fin (C.gates i).fanIn → BitString n → ZMod 3), (∀ (k : Fin (C.gates i).fanIn), v k ∈ lowDegree n D) → (fun (x : BitString n) => A i fun (k : Fin (C.gates i).fanIn) => v k x) ∈ lowDegree n (2 * ℓ * D)) (hbad : ∀ (i : Fin G), ∀ x ∉ Bad, (A i fun (k : Fin (C.gates i).fanIn) => bitVal ((C.gates i).negated k ^^ C.wireValue x ((C.gates i).inputs k))) = bitVal ((C.gates i).eval (C.wireValue x))) (w : Fin (n + G)) : ∃ P ∈ lowDegree n ((2 * ℓ) ^ C.wireDepth w), ∀ x ∉ Bad, P x = bitVal (C.wireValue x w)

Approximators of every wire, given gate approximators correct off Bad.

theorem Complexity.Smolensky.exists_output_approx {n G M : ℕ} [NeZero n] [NeZero M] (C : Circuit (Basis.unboundedAndOrMod 3) n M G) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (Bad : Finset (BitString n)) (A : (i : Fin G) → (Fin (C.gates i).fanIn → ZMod 3) → ZMod 3) (hdeg : ∀ (i : Fin G) (D : ℕ) (v : Fin (C.gates i).fanIn → BitString n → ZMod 3), (∀ (k : Fin (C.gates i).fanIn), v k ∈ lowDegree n D) → (fun (x : BitString n) => A i fun (k : Fin (C.gates i).fanIn) => v k x) ∈ lowDegree n (2 * ℓ * D)) (hbad : ∀ (i : Fin G), ∀ x ∉ Bad, (A i fun (k : Fin (C.gates i).fanIn) => bitVal ((C.gates i).negated k ^^ C.wireValue x ((C.gates i).inputs k))) = bitVal ((C.gates i).eval (C.wireValue x))) (j : Fin M) (Aout : (Fin (C.outputs j).fanIn → ZMod 3) → ZMod 3) (hdegOut : ∀ (D : ℕ) (v : Fin (C.outputs j).fanIn → BitString n → ZMod 3), (∀ (k : Fin (C.outputs j).fanIn), v k ∈ lowDegree n D) → (fun (x : BitString n) => Aout fun (k : Fin (C.outputs j).fanIn) => v k x) ∈ lowDegree n (2 * ℓ * D)) (hbadOut : ∀ x ∉ Bad, (Aout fun (k : Fin (C.outputs j).fanIn) => bitVal ((C.outputs j).negated k ^^ C.wireValue x ((C.outputs j).inputs k))) = bitVal ((C.outputs j).eval (C.wireValue x))) : ∃ P ∈ lowDegree n ((2 * ℓ) ^ C.outputDepth j), ∀ x ∉ Bad, P x = bitVal (C.eval x j)

The approximation theorem for a single output gate.

theorem Complexity.Smolensky.exists_lowDegree_approx_internal {n G d ℓ : ℕ} [NeZero n] (C : Circuit (Basis.unboundedAndOrMod 3) n 1 G) (hdepth : C.depth ≤ d) (hℓ : 1 ≤ ℓ) : ∃ P ∈ lowDegree n ((2 * ℓ) ^ d), {x : BitString n | P x ≠ bitVal (C.eval x 0)}.card * 2 ^ ℓ ≤ C.size * 2 ^ n

Smolensky's approximation theorem. A single-output AND/OR/MOD_3 circuit of depth at most d agrees with some function of degree at most (2ℓ)^d on all but at most size · 2^n / 2^ℓ inputs.