The exact leading homogeneous coefficient height supplies the full scaling gain in every dimension.

theorem CCDN.scaledHomogenize_leading_height_lower {n : ℕ} (f : MvPolynomial (Fin n) ℤ) {h : ℤ} (hh : 1 ≤ h) : ↑h ^ f.totalDegree * ↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f)) ≤ ↑(integerCoefficientHeight (scaledHomogenize f.totalDegree h f))

For h ≥ 1, the scaled homogenization of f in degree d = f.totalDegree has coefficient height at least h ^ d times the coefficient height of the top homogeneous component of f.

theorem CCDN.leading_height_one_le {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f ≠ 0) : 1 ≤ ↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f))

The top homogeneous component of a nonzero integer polynomial has coefficient height at least 1.