The ordinary homogenization provides an affine auxiliary without a scaling-prime hypothesis and transfers the coefficient-height dichotomy.

theorem CCDN.integerCoefficientHeight_scaledHomogenize_one {n : ℕ} (d : ℕ) (f : MvPolynomial (Fin n) ℤ) : integerCoefficientHeight (scaledHomogenize d 1 f) = integerCoefficientHeight f

The ordinary homogenization (scaling factor one) of an integer polynomial has the same coefficient height as the polynomial.

theorem CCDN.unscaled_auxiliary_not_dvd {n M : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf0 : f ≠ 0) (hprim : PrimitiveIntegerPolynomial f) (G : MvPolynomial (Fin (n + 1)) ℤ) (hGhom : G.IsHomogeneous M) (hGnd : ¬scaledHomogenize f.totalDegree 1 f ∣ G) : ¬f ∣ (homogeneousSlice n 1) G

If a form G is not divisible by the ordinary homogenization of a nonzero primitive integer polynomial f, then its dehomogenization at x₀ = 1 is not divisible by f.

theorem CCDN.unscaled_affine_auxiliary {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) {B : ℝ} (hB : 1 ≤ B) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ hypersurfaceAuxiliaryDegreeBound n f.totalDegree B (hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree 1 f)) ↑(integerCoefficientHeight f)

Ordinary homogenization gives an auxiliary in every affine box, with the height and bad-prime factor of the unscaled model.

theorem CCDN.affine_coefficient_height_dichotomy {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf0 : f ≠ 0) (hprim : PrimitiveIntegerPolynomial f) {B : ℝ} (hB : 1 ≤ B) : Real.log ↑(integerCoefficientHeight f) ≤ ↑((n + f.totalDegree).choose f.totalDegree) * Real.log ↑((n + f.totalDegree).choose f.totalDegree) + ↑((n + f.totalDegree).choose f.totalDegree) * ↑f.totalDegree * Real.log B ∨ ∃ (g : MvPolynomial (Fin n) ℤ), IsBoxAuxiliary f g B ∧ g.totalDegree ≤ f.totalDegree

Either the affine equation has controlled coefficient height, or a degree-at-most-d nonmultiple vanishes on every bounded integer zero.