The geometric bad-prime charge in arbitrary dimension is controlled by coefficient height, via an explicit integer witness with bounded height.
A nonzero bad-prime witness obtained by evaluating the universal plane polynomial on a bounded integer grid.
Explicit height estimates for the evaluated universal bad-prime witness.
theorem
CCDN.exists_hypersurface_bad_prime_height_witness
{L : Type u_1}
{σ : Type u_2}
[Field L]
[CharZero L]
[IsAlgClosed L]
[Fintype σ]
(f : MvPolynomial (Option σ) ℤ)
(hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f))
(hpos : 0 < f.totalDegree)
(H : ℝ)
(hH : 1 ≤ H)
(hcoeff : CoefficientHeightLE f H)
:
∃ (D : ℤ),
0 < D ∧ Real.log ↑D ≤ 27 * ↑f.totalDegree ^ 4 * (hypersurfaceHeightConstant (Fintype.card (Option σ)) * (1 + Real.log H / ↑f.totalDegree ^ 2)) ∧ ∀ (p : ℕ), f.totalDegree < p → HypersurfaceBadReduction f p → ↑p ∣ D
An effective positive integer detecting every bad prime above the degree.
theorem
CCDN.hypersurface_bad_prime_charge
{L : Type u_1}
{σ : Type u_2}
[Field L]
[CharZero L]
[IsAlgClosed L]
[Fintype σ]
(f : MvPolynomial (Option σ) ℤ)
(hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f))
(hpos : 0 < f.totalDegree)
(H : ℝ)
(hH : 1 ≤ H)
(hcoeff : CoefficientHeightLE f H)
(P : Finset ℕ)
(hP : ∀ p ∈ P, HypersurfaceBadReduction f p)
(hcut : ∀ p ∈ P, stepanovThreshold f.totalDegree < p)
:
∑ p ∈ P, Real.log ↑p / ↑p ≤ Real.log (hypersurfaceHeightConstant (Fintype.card (Option σ)) * (1 + Real.log H / ↑f.totalDegree ^ 2)) + 2 * mertensError + 1
The logarithmic charge bound for any finite family of bad primes. This includes degree-dropping primes as well as geometric reducibility.
theorem
CCDN.hypersurface_bad_prime_factor_max
{L : Type u_1}
{σ : Type u_2}
[Field L]
[CharZero L]
[IsAlgClosed L]
[Fintype σ]
(f : MvPolynomial (Option σ) ℤ)
(hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f))
(hpos : 0 < f.totalDegree)
(H : ℝ)
(hH : 1 ≤ H)
(hcoeff : CoefficientHeightLE f H)
(P : Finset ℕ)
(hP : ∀ p ∈ P, HypersurfaceBadReduction f p)
(hcut : ∀ p ∈ P, stepanovThreshold f.totalDegree < p)
:
primeSetFactor P ≤ 2 * Real.exp (2 * mertensError + 1) * hypersurfaceHeightConstant (Fintype.card (Option σ)) * max (Real.log H / ↑f.totalDegree ^ 2) 1
The maximum formulation of CCDN Corollary 3.2.3, with an explicit constant depending only on the number of variables.