Combine the two height ranges under the paper's explicit leading-coefficient position condition. The main term retains the bad-prime factor of any finite prime set whose normalized comparison holds.

theorem CCDN.hypersurfaceSmallThreshold_position {n d : ℕ} {B H L A T : ℝ} (hd : 0 < d) (hB : 0 ≤ B) (hH : 0 < H) (hL : 0 < L) (hA : 0 ≤ A) (hposition : Real.log H ≤ Real.log L + T * ↑d * degreeRoot n d) : hypersurfaceSmallThreshold n d B L A ≤ Real.exp (T / (↑n + 1)) * hypersurfaceSmallThreshold n d B H A

Replacing the coefficient height H by the leading height L in the small-height threshold costs at most a factor exp (T / (n + 1)), provided log H ≤ log L + T d d^(1/(n+1)).

noncomputable def CCDN.hypersurfacePositionedAuxiliaryConstant (n : ℕ) (T : ℝ) : ℝ

Explicit constant for the positioned absolutely irreducible case.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.positioned_auxiliary_degree_of_comparison {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) {B : ℝ} {z : Fin t → IntPoint (n + 3)} (hzB : IsPrimitiveBoxZeroFamily f B z) (bad : Finset ℕ) (hcomp : AuxiliaryRankComparison order f d z bad) (T : ℝ) (hT : 0 ≤ T) (hposition : Real.log H ≤ Real.log |↑(order.leadingCoeff f)| + T * ↑d * degreeRoot n d) : ∃ (M : ℕ), ↑M ≤ hypersurfacePositionedAuxiliaryConstant n T * auxDegreeBound n d B (primeSetFactor bad) H ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), IsPointAuxiliary f g M z

The coefficient-sensitive auxiliary theorem for an absolutely irreducible homogeneous equation satisfying explicit leading-coefficient positioning, for any finite prime set bad for which the normalized comparison holds. Both height ranges and the degree are constructed.