The geometric bad-prime charge for arbitrary integer plane equations. The proof combines bounded integral normalization, coefficient growth and an integer minor witness; reducibility is tested over the residue field's algebraic closure.

theorem CCDN.exists_plane_bad_prime_witness {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (d : ℕ) (hd : 1 ≤ d) (f : Polynomial (Polynomial ℤ)) (hdeg : bivariateTotalDegree f = d) (hir : Irreducible ((bivariateMap (Int.castRingHom F)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : BivariateCoefficientBound f H) : ∃ (D : ℤ), 0 < D ∧ Real.log ↑D ≤ 189 * ↑d ^ 4 * (1 + Real.log H / ↑d ^ 2) ∧ ∀ (p : ℕ), d < p → BivariateBadReduction f d p → ↑p ∣ D

Every absolutely irreducible integer plane equation has a coefficient- controlled positive integer detecting all geometric bad primes above d.

theorem CCDN.plane_geometric_bad_prime_charge {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (d : ℕ) (hd : 1 ≤ d) (f : Polynomial (Polynomial ℤ)) (hdeg : bivariateTotalDegree f = d) (hir : Irreducible ((bivariateMap (Int.castRingHom F)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : BivariateCoefficientBound f H) (P : Finset ℕ) (hbad : ∀ p ∈ P, BivariateBadReduction f d p) (hlo : ∀ p ∈ P, stepanovThreshold ↑d < ↑p) : ∑ p ∈ P, Real.log ↑p / ↑p ≤ Real.log (1 + Real.log H / ↑d ^ 2) + Real.log 7 + 2 * mertensError + 1

Geometric bad primes above 27*d^4 have logarithmic charge controlled by log(1+log(H)/d²) plus an absolute constant.