Coefficient-controlled bad primes for homogeneous projective evaluation matrices. Good reduction of a full-degree affine chart implies good reduction of the entire projective equation.

theorem CCDN.projective_determinant_log_lower_height {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {s N d M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) {H : ℝ} (hchart : IsBoundedPlaneCurve K ((affineChart 2) f) d H) {F : Fin N → MvPolynomial (Fin 3) ℤ} {z : Fin s → IntPoint 3} (hev : IsIndependentEvaluation f M F z) : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑d - Real.log (1 + Real.log H / ↑d ^ 2) - heightDeterminantError projectivePlaneDeterminantConstant) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)))

The global projective determinant lower bound, with the bad-prime charge controlled by the coefficient height H of the affine chart.