CCDN Theorem 3.1.1 for irreducible integer homogeneous equations. The constant is fixed before the equation, degree and radius are chosen.

theorem CCDN.hypersurfaceAbsoluteAuxiliaryConstant_one_le (n : ℕ) : 1 ≤ hypersurfaceAbsoluteAuxiliaryConstant n

The constant hypersurfaceAbsoluteAuxiliaryConstant n is at least 1.

theorem CCDN.hypersurface_projective_auxiliary {n d : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible f) {B : ℝ} (hB : 1 ≤ B) : ∃ (M : ℕ), ↑M ≤ hypersurfaceAuxiliaryDegreeBound n d B (hypersurfaceBadPrimeFactor f) ↑(integerCoefficientHeight f) ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (x : ProjectivePoint (n + 2)), Projectivization.mulHeight x ≤ B → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g)) ∧ ¬f ∣ g

CCDN Theorem 3.1.1: the full coefficient-sensitive auxiliary-polynomial bound, including equations that split over an algebraic closure.