Sharp prime-power and global prime-sum bounds for projective plane evaluation matrices. The excluded-prime set is explicit.

A sharp finite-field count for an irreducible homogeneous plane curve. Chart irreducibility, its full degree and the infinity correction are proved; the affine input is the formalized Stepanov estimate.

theorem CCDN.projective_plane_finite_field_card_bound {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hsize : stepanovThreshold ↑d < ↑p) : ↑(Fintype.card ↑(ProjectivePlaneResidue f p)) ≤ ↑p + projectivePlaneResidueConstant * ↑d ^ 2 * √↑p

For a homogeneous integer polynomial f of degree d ≥ 2 with irreducible reduction modulo a prime p > 27 d⁴, the reduced plane curve has at most p + projectivePlaneResidueConstant · d² · √p points over 𝔽_p.

theorem CCDN.projectivePlaneTotalMultiplicity_le {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hsize : stepanovThreshold ↑d < ↑p) : ↑(projectivePlaneTotalMultiplicity f hf ⋯) ≤ ↑p + (projectivePlaneDeterminantConstant + 1) * ↑d ^ 2 * √↑p

For a homogeneous integer polynomial f of degree d ≥ 2 with irreducible reduction modulo a prime p > 27 d⁴, the total residue multiplicity of f mod p is at most p + (projectivePlaneDeterminantConstant + 1) · d² · √p.

theorem CCDN.projective_determinant_log_lower_at_rank {s N d M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) {F : Fin N → MvPolynomial (Fin 3) ℤ} {z : Fin s → IntPoint 3} (hev : IsIndependentEvaluation f M F z) (bad : Finset ℕ) (hred : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 s) \ bad, stepanovThreshold ↑d < ↑p → Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑d - ∑ p ∈ bad, Real.log ↑p / ↑p - degreeFourDeterminantError projectivePlaneDeterminantConstant) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)))

Plane case of CCDN Proposition 3.2.6 at a single rank: for an independent evaluation of forms at s primitive zeros of a degree-d ≥ 2 plane curve whose reductions modulo primes 27 d⁴ < p ≤ s outside bad are irreducible, the logarithm of the gcd of the maximal minors is at least s² / 2 · (log s - 4 log d - ∑_{p ∈ bad} log p / p - E), with the explicit constant E = degreeFourDeterminantError projectivePlaneDeterminantConstant.