The finite interpolation step for condenser expansion

For any fixed feature values, fewer than A * K evaluation constraints admit a nonzero family of K coefficient polynomials, each of degree less than A. In the Guruswami--Umans--Vadhan expansion proof (2009), Section 3.1, the features are the first K base-h monomials evaluated at a neighbor tuple. The parameter K is the actual source size, not the maximum h^m allowed by the construction.

This theorem proves existence of the interpolating witness by linear algebra. It is part of the expansion proof, not an algorithm used to evaluate the condenser. Removing common modulus factors and proving the root-count bound are separate steps.

theorem Algebraic.Cutwidth.Extractor.exists_polynomial_interpolant {F : Type u_1} {X : Type u_2} [Field F] {A K : ℕ} (T : Finset X) (seed : X → F) (weight : X → Fin K → F) (budget : T.card < A * K) : ∃ (p : Fin K → Polynomial F), p ≠ 0 ∧ (∀ (j : Fin K), (p j).degree < ↑A) ∧ ∀ x ∈ T, ∑ j : Fin K, Polynomial.eval (seed x) (p j) * weight x j = 0

Fewer scalar constraints than coefficients leave a nonzero interpolant. The constraint type is arbitrary; source seeds and feature weights are fixed before the coefficient family is chosen.