The global determinant bound in higher dimension, with its reduction hypotheses verified by the bad-prime set and its coefficient-height control.

theorem CCDN.exists_hypersurface_determinant_log_lower {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n s N d M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) {F : Fin N → MvPolynomial (Fin (n + 3)) ℤ} {z : Fin s → IntPoint (n + 3)} (hev : IsIndependentEvaluation f M F z) : ∃ (bad : Finset ℕ), (∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) ∧ hypersurfaceRankLowerBound n s d (∑ p ∈ bad, Real.log ↑p / ↑p) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)))

The rank-cutoff determinant estimate with the exact constructed bad-prime set. This is the common-degree maximal-minor form of CCDN Proposition 3.2.6.

noncomputable def CCDN.hypersurfaceHeightDeterminantError (n : ℕ) : ℝ

The height-dependent error contains only dimension constants.

Equations

• CCDN.hypersurfaceHeightDeterminantError n = CCDN.hypersurfaceDeterminantError n + (↑n + 1) * (Real.log (CCDN.hypersurfaceHeightConstant (n + 3)) + 2 * CCDN.mertensError + 1)

theorem CCDN.hypersurface_determinant_log_lower_height {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n s N d M : ℕ} (hs : 0 < s) (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) {F : Fin N → MvPolynomial (Fin (n + 3)) ℤ} {z : Fin s → IntPoint (n + 3)} (hev : IsIndependentEvaluation f M F z) : factorialRoot n / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) * (Real.log ↑s - (↑n + 1) * (4 * Real.log ↑d + Real.log (1 + Real.log H / ↑d ^ 2)) - hypersurfaceHeightDeterminantError n) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)))

The full higher-dimensional logarithmic determinant lower bound, including the local counts and the geometric bad-prime charge.