Auxiliary polynomials in the large-height range. The degree is O_{n,T}(d^(4-1/(n+1))); the leading-coefficient positioning cost is explicit.

theorem CCDN.hypersurface_auxiliary_large_height_degree {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n d t : ℕ} (order : MonomialOrder (Fin (n + 3))) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (z : Fin t → IntPoint (n + 3)) (hprim : ∀ (i : Fin t), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) {B : ℝ} (hB : 1 ≤ B) (hbox : ∀ (i : Fin t), InBox (z i) B) (T : ℝ) (hT : 0 ≤ T) (hheight : 2 * ↑d * (↑n + 2) * Real.log B ≤ Real.log H) (hposition : Real.log H ≤ Real.log |↑(order.leadingCoeff f)| + T * ↑d * degreeRoot n d) : ∃ (M : ℕ), ↑M ≤ (8 * (↑n + 2) + Real.exp (hypersurfaceLargeHeightError (n + 1) (hypersurfaceNormalizedError n) T) + 2) * ↑d ^ (4 - 1 / (↑n + 1)) ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (i : Fin t), (MvPolynomial.eval (z i)) g = 0) ∧ ¬f ∣ g

Select a bounded integer degree in the large-height range. The bound is independent of the box radius and the equation's coefficient height.