Polynomial gates preserve local linear realizations

Taking formal derivatives at zero assigns a coefficient vector to every original wire. The vector at a gate lies in the span of its argument vectors, irrespective of the gate polynomial's degree or constant term. Thus the original program graph supports a linear realization. Over an infinite field, computing a linear map as a function guarantees that the output vectors are exactly its matrix rows.

The infinite-field hypothesis is needed only for the output identification, since distinct polynomials can agree on every point of a finite field.

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.realization {F : Type u_1} [Field F] {σ : Signature} {n s : ℕ} {I : Interpretation σ F} (hI : IsPolynomial I) (p : Program σ n s) : Linear.Realization p F

Every polynomial interpretation gives a local linear realization on the same graph.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.realization_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) : (realization hI c.program).value (c.outputs i) = M i

A polynomial circuit computing a linear map over an infinite field has the exact target rows at the outputs of its local linear realization.