Formal linearization of polynomial gate computations

The derivative-at-zero vector of a substitution lies in the span of the substituted polynomials' vectors. Polynomial induction proves this directly using the product rule.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_C {F : Type u_1} [Field F] {n : ℕ} (a : F) : linearPart (MvPolynomial.C a) = 0

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_add {F : Type u_1} [Field F] {n : ℕ} (p q : MvPolynomial (Fin n) F) : linearPart (p + q) = linearPart p + linearPart q

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_mul {F : Type u_1} [Field F] {n : ℕ} (p q : MvPolynomial (Fin n) F) : linearPart (p * q) = (MvPolynomial.eval fun (x : Fin n) => 0) q • linearPart p + (MvPolynomial.eval fun (x : Fin n) => 0) p • linearPart q

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_X {F : Type u_1} [Field F] {n : ℕ} (j : Fin n) : linearPart (MvPolynomial.X j) = Pi.single j 1

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_aeval_mem_span {F : Type u_1} [Field F] {n arity : ℕ} (args : Fin arity → MvPolynomial (Fin n) F) (q : MvPolynomial (Fin arity) F) : linearPart ((MvPolynomial.aeval args) q) ∈ Submodule.span F (Set.range fun (i : Fin arity) => linearPart (args i))

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.gatePolynomial_eval {F : Type u_1} [Field F] {σ : Signature} {I : Interpretation σ F} (hI : IsPolynomial I) (op : σ.Op) (x : Fin (σ.Arity op) → F) : (MvPolynomial.eval x) (hI.gatePolynomial op) = I op x

def Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.evaluationHom {F : Type u_1} [Field F] {σ : Signature} {n : ℕ} {I : Interpretation σ F} (hI : IsPolynomial I) (x : Fin n → F) : Homomorphism (hI.formalInterpretation n) I

Evaluating formal wire polynomials commutes with every original gate operation.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.evaluationHom hI x = { map := ⇑(MvPolynomial.eval x), homomorphic := ⋯ }

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.wirePolynomial_eval {F : Type u_1} [Field F] {σ : Signature} {n s : ℕ} {I : Interpretation σ F} (hI : IsPolynomial I) (p : Program σ n s) (x : Fin n → F) (w : Wire n s) : (MvPolynomial.eval x) (hI.wirePolynomial p w) = p.trace I x w

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_wirePolynomial_gate {F : Type u_1} [Field F] {σ : Signature} {n s : ℕ} {I : Interpretation σ F} (hI : IsPolynomial I) (p : Program σ n s) (g : Fin s) : linearPart (hI.wirePolynomial p (Wire.gate g)) ∈ Submodule.span F (Set.range fun (i : Fin (σ.Arity (p.lines g).op)) => linearPart (hI.wirePolynomial p ((p.lines g).wires i)))

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.eval_linearPolynomial {F : Type u_1} [Field F] {n : ℕ} (row x : Fin n → F) : (MvPolynomial.eval x) (linearPolynomial row) = row ⬝ᵥ x

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.linearPart_linearPolynomial {F : Type u_1} [Field F] {n : ℕ} (row : Fin n → F) : linearPart (linearPolynomial row) = row

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.Internal.wirePolynomial_output {F : Type u_1} [Field F] {σ : Signature} {n m : ℕ} [Infinite F] {I : Interpretation σ F} (hI : IsPolynomial I) (c : Circuit σ n m) (M : Matrix (Fin m) (Fin n) F) (hc : c.Computes I fun (x : Fin n → F) => M.mulVec x) (i : Fin m) : hI.wirePolynomial c.program (c.outputs i) = linearPolynomial (M i)