A nonzero coefficient family satisfying fewer linear constraints

The interpolation family has A * K scalar coefficients. Evaluation at each constraint is linear in those coefficients, so fewer than A * K constraints leave a nonzero kernel vector. Grouping its coefficients gives K polynomials of degree less than A.

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