The sharp projective finite-field count and its singular multiplicity correction. This discharges the count in CCDN Lemma 2.7.
theorem
CCDN.projective_hypersurface_finite_field_bound
{n d : ℕ}
(p : ℕ)
[Fact (Nat.Prime p)]
(f : MvPolynomial (Fin (n + 3)) (ZMod p))
(hf : f.IsHomogeneous d)
(hd : 0 < d)
(hir : Irreducible ((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) f))
(hsize : stepanovThreshold ↑d < ↑p)
:
An absolutely irreducible form f of degree d > 0 in n + 3 variables over ZMod p, with
p above the threshold 27 * d ^ 4, has at most
p ^ (n + 1) + projectiveHypersurfaceResidueConstant * d ^ 2 * p ^ n * √p projective zeros.
theorem
CCDN.projective_hypersurface_totalMultiplicity_bound
{n p d : ℕ}
[Fact (Nat.Prime p)]
(f : MvPolynomial (Fin (n + 3)) ℤ)
(hf : f.IsHomogeneous d)
(hd : 0 < d)
(hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0)
(hir :
Irreducible
((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p))))
((MvPolynomial.map (Int.castRingHom (ZMod p))) f)))
(hsize : stepanovThreshold ↑d < ↑p)
:
CCDN Lemma 2.7 for the total multiplicity of the projective residue space. The constant depends only on dimension, and all counting inputs are proved. Degree one is included using the exact multiplicity bounds.