Vanishing maximal determinants on a standard-monomial family produce an integer auxiliary outside the original principal ideal.

theorem CCDN.exists_standard_auxiliary_of_zero_determinants {n N t M : ℕ} (f : MvPolynomial (Fin n) ℚ) (mon : Fin N → Fin n →₀ ℕ) (hmon : Function.Injective mon) (hstd : ∀ (j : Fin N), mon j ∈ (Ideal.span {f}).standardExponents MonomialOrder.degLex) (hdegree : ∀ (j : Fin N), Finsupp.degree (mon j) ≤ M) (x : Fin t → IntPoint n) (hdet : ∀ (a : Fin N → Fin t), (evaluationMatrix mon (x ∘ a)).det = 0) : ∃ (g : MvPolynomial (Fin n) ℤ), g ≠ 0 ∧ ¬f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ g.totalDegree ≤ M ∧ ∀ (i : Fin t), (MvPolynomial.eval (x i)) g = 0

If mon is an injective family of N standard monomials (for the degree-lexicographic order) of the ideal generated by f over ℚ, all of degree at most M, and every N × N evaluation determinant of these monomials at points chosen from x vanishes, then there is a nonzero integer polynomial g of degree at most M, vanishing at every point x i, whose image over ℚ is not divisible by f.