The ordinary homogenization attains the affine box exponent on every polynomial range in the degree, with both terms of the minimum retained.
The coefficient height of the leading homogeneous component of an integer polynomial is at most the coefficient height of the polynomial itself.
theorem
CCDN.unscaled_affine_auxiliary_minimum
{n k : ℕ}
(f : MvPolynomial (Fin (n + 2)) ℤ)
(hprim : PrimitiveIntegerPolynomial f)
(hir : Irreducible f)
(hd : 0 < f.totalDegree)
{S B : ℝ}
(hS : 1 ≤ S)
(hB : 1 ≤ B)
(hbound : B ≤ S * (↑f.totalDegree + 1) ^ k)
:
∃ (g : MvPolynomial (Fin (n + 2)) ℤ),
IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ affineMinimumAuxiliaryBound n f.totalDegree (Real.exp (Real.log S + ↑k * (↑n + 2))) B
(↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f)))
(hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree 1 f))
An affine auxiliary with the minimum degree bound in the polynomial box range. The constant coefficient is arbitrary.