Uniform coefficient absorption and affine-box estimates for the auxiliary theorem with an irreducible leading homogeneous form.

theorem CCDN.hypersurface_badPrime_fractional_height_bound {m r d : ℕ} (f : MvPolynomial (Fin (m + 1)) ℤ) (hf : f ≠ 0) (hdegree : f.totalDegree = d) (hr : 0 < r) (hd : 0 < d) : hypersurfaceBadPrimeFactor f / ↑(integerCoefficientHeight f) ^ (1 / (↑r * ↑d * ↑d ^ (1 / ↑r))) ≤ ↑r * Real.exp (2 * mertensError + 1) * hypersurfaceHeightConstant (m + 1)

For a nonzero integer polynomial f of degree d > 0 with coefficient height H and for r > 0, the bad-prime factor of f divided by H^(1/(r d d^(1/r))) is bounded by a constant depending only on r and the number of variables.

theorem CCDN.affineAuxiliaryDegreeExpression_le_of_badPrime_ratio (n : ℕ) {d : ℕ} (hd : 0 < d) {B L b K : ℝ} (hB : 1 ≤ B) (hL : 1 ≤ L) (hratio : b / L ^ (1 / ((↑n + 1) * ↑d * ↑d ^ (1 / (↑n + 1)))) ≤ K) : affineAuxiliaryDegreeExpression n d B L b ≤ (K + 2) * ↑d ^ (4 - 1 / (↑n + 1)) * B ^ (1 / ↑d ^ (1 / (↑n + 1)))

A uniform bound on the coefficient-weighted bad-prime factor removes both the coefficient dependence and the logarithmic box term.