Degree and evaluation bounds for the substituted interpolation polynomial

Reduction bounds each source-power coordinate by one less than the modulus degree. A base-h monomial uses at most h - 1 copies of each coordinate, so its degree grows by at most (n - 1) * (h - 1) * m. Multiplication by a coefficient polynomial of degree below A leaves degree below that quantity plus A. No bound on the unreduced source polynomial is needed here.

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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)