Bounded rational zeros either admit a degree-d auxiliary nonmultiple, or control the defining equation's coefficient height by an explicit finite-dimensional interpolation bound.

Bombieri--Vaaler for complete homogeneous evaluation matrices. The defining equation supplies rank deficiency, and selected rows span the whole point set.

theorem CCDN.homogeneous_same_degree_coefficient_le_of_dvd {n d : ℕ} {f g : MvPolynomial (Fin n) ℤ} (hf : f.IsHomogeneous d) (hg : g.IsHomogeneous d) (hg0 : g ≠ 0) (hdiv : f ∣ g) (m : Fin n →₀ ℕ) : |↑(f.coeff m)| ≤ |↑(g.coeff m)|

If an integer form f of degree d divides a nonzero integer form g of the same degree, then every coefficient of f is bounded in absolute value by the corresponding coefficient of g, since g is a nonzero integer multiple of f.

theorem CCDN.projective_coefficient_height_dichotomy {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) {B : ℝ} (hB : 1 ≤ B) : Real.log ↑(integerCoefficientHeight f) ≤ ↑((n + d).choose d) * Real.log ↑((n + d).choose d) + ↑((n + d).choose d) * ↑d * Real.log B ∨ ∃ (g : MvPolynomial (Fin (n + 1)) ℤ), IsProjectiveAuxiliary f g d B

A quantitative coefficient-height dichotomy on the complete bounded projective zero set. The height branch has log(H)<=N log(N)+d N log(B).