Homogeneous equations give nonzero relations on the complete homogeneous evaluation matrix and hence strictly deficient row rank.

theorem CCDN.homogeneous_eq_sum_coeff {K : Type u_1} [CommSemiring K] {n M : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) : f = ∑ j : Fin ((n + M).choose M), (MvPolynomial.monomial (homogeneousMonomials n M j)) (f.coeff (homogeneousMonomials n M j))

A homogeneous polynomial of degree M in n + 1 variables is the sum of its terms over the degree-M monomials enumerated by homogeneousMonomials n M.

theorem CCDN.homogeneous_independent_evaluation_rows {n d M t : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) : ∃ (s : ℕ) (a : Fin s → Fin t), Function.Injective a ∧ LinearIndependent ℚ ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row ∧ Submodule.span ℚ (Set.range ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row) = Submodule.span ℚ (Set.range ((evaluationMatrix (homogeneousMonomials n M) points).map Int.cast).row) ∧ s < (n + M).choose M

Select a spanning family of independent evaluation rows. The homogeneous equation, padded to degree M, proves strict rank deficiency.