The quotient-field root bound in GUV expansion

The first K interpolation monomials become powers with exponents below K in the quotient by a supplied irreducible modulus. A coefficient not divisible by the modulus makes this polynomial nonzero. It has fewer than K roots, and distinct bounded-degree source polynomials give distinct quotient classes.

This is the final algebraic step of Guruswami, Umans, and Vadhan (2009), Theorem 3.3: https://salil.seas.harvard.edu/sites/g/files/omnuum4266/files/salil/files/acm2009.pdf. The quotient field here is used in the semantic proof. Its Mathlib instance does not provide an encoded field representation or a uniform evaluator.

theorem Algebraic.Cutwidth.Extractor.substitutedSum_quotient_eval {F : Type u_1} [Field F] {h K m : ℕ} (E : Polynomial F) (monic : E.Monic) (bound : K ≤ h ^ m) (p : Fin K → Polynomial F) (f : Polynomial F) : Polynomial.eval ((AdjoinRoot.mk E) f) (∑ j : Fin K, (Polynomial.monomial ↑j) ((AdjoinRoot.mk E) (p j))) = (AdjoinRoot.mk E) (substitutedSum E h m p f)

Evaluation of the quotient polynomial agrees with the class of the substituted interpolation sum. The exponent cap retains the actual K.

theorem Algebraic.Cutwidth.Extractor.card_lt_of_quotient_polynomial_roots {F : Type u_1} [Field F] {K : ℕ} (E : Polynomial F) (monic : E.Monic) (irreducible : Irreducible E) (p : Fin K → Polynomial F) (primitive : ∃ (j : Fin K), ¬E ∣ p j) (P : Finset (Polynomial F)) (source : ∀ f ∈ P, f.degree < E.degree) (roots : ∀ f ∈ P, Polynomial.eval ((AdjoinRoot.mk E) f) (∑ j : Fin K, (Polynomial.monomial ↑j) ((AdjoinRoot.mk E) (p j))) = 0) : P.card < K

A primitive coefficient family gives fewer than K distinct bounded-degree source polynomials at which its quotient polynomial vanishes.