The determinant lower bound, with the bad-prime input given by the coefficient-controlled witness. The sharp finite-field point estimate is an explicit hypothesis.

noncomputable def CCDN.heightDeterminantError (C : ℝ) : ℝ

degreeFourDeterminantError C plus the constant part log 7 + 2 mertensError + 1 of the bad-prime charge of exists_plane_bad_prime_set.

Equations

• CCDN.heightDeterminantError C = CCDN.degreeFourDeterminantError C + Real.log 7 + 2 * CCDN.mertensError + 1

theorem CCDN.singular_determinant_log_lower_height {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {s N : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin 2) ℤ) (hd : 0 < f.totalDegree) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (g : Fin N → MvPolynomial (Fin 2) ℤ) (z : Fin s → Fin 2 → ℤ) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (hrows : LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k)).map Int.cast).row) {C : ℝ} (hC : 0 ≤ C) (hcount : PlaneResidueCountBound C f.totalDegree f) : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑f.totalDegree - Real.log (1 + Real.log H / ↑f.totalDegree ^ 2) - heightDeterminantError C) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k)))

The excluded-prime set and its charge are derived from the absolute irreducibility and coefficient-height hypotheses. The only local arithmetic hypothesis is the stated sharp finite-field point bound.