The substituted interpolation polynomial has bounded degree

After replacing each coordinate by a source power reduced modulo a supplied monic modulus, the interpolation polynomial has degree below A + (E.natDegree - 1) * (h - 1) * m. Its evaluation is exactly the weighted sum of feature values constrained by interpolation. These are the degree and evaluation steps in Guruswami--Umans--Vadhan (2009), Section 3.1.

The modulus need not be irreducible for these statements. The source is any polynomial: its degree is reduced before the monomials are substituted. The subsequent root-count proof separately requires the appropriate field and source-injectivity hypotheses.

theorem Algebraic.Cutwidth.Extractor.substitutedSum_eval {F : Type u_1} [CommRing F] {K : ℕ} (E : Polynomial F) (h m : ℕ) (p : Fin K → Polynomial F) (f : Polynomial F) (y : F) : Polynomial.eval y (substitutedSum E h m p f) = ∑ j : Fin K, Polynomial.eval y (p j) * digitMonomial h ↑j fun (i : Fin m) => Polynomial.eval y (f ^ h ^ ↑i %ₘ E)

Polynomial substitution followed by evaluation equals evaluation of the weighted monomial features used by the interpolation constraints.

theorem Algebraic.Cutwidth.Extractor.substitutedSum_natDegree_le {F : Type u_1} [CommRing F] {K A h m : ℕ} (E : Polynomial F) (p : Fin K → Polynomial F) (f : Polynomial F) (monic : E.Monic) (base : 0 < h) (coeff : ∀ (j : Fin K), (p j).degree < ↑A) : (substitutedSum E h m p f).natDegree ≤ A - 1 + (E.natDegree - 1) * (h - 1) * m

Each reduced coordinate has degree at most E.natDegree - 1, so the digit sum gives this uniform bound on the substituted polynomial.

theorem Algebraic.Cutwidth.Extractor.substitutedSum_degree_lt {F : Type u_1} [CommRing F] {K A h m : ℕ} (E : Polynomial F) (p : Fin K → Polynomial F) (f : Polynomial F) (monic : E.Monic) (positive : 0 < A) (base : 0 < h) (coeff : ∀ (j : Fin K), (p j).degree < ↑A) : (substitutedSum E h m p f).degree < ↑(A + (E.natDegree - 1) * (h - 1) * m)

The strict-degree form used to deduce a zero polynomial from many roots.