The singular multiplicity correction for projective hypersurfaces. Chart coordinates inject each selected residue class into an affine singular locus, whose codimension-two point bound is proved by interpolation.

The singular points of an irreducible hypersurface satisfy a coefficient-uniform codimension-two finite-field bound.

theorem CCDN.projectiveHypersurfaceTotalMultiplicity_le_card_add_correction {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hchar : d < p) : projectiveHypersurfaceTotalMultiplicity f hf ⋯ ≤ Fintype.card ↑(ProjectiveHypersurfaceResidue f p) + (n + 3) * (n + 4) ^ n * d ^ 2 * (d - 1) * p ^ n

Singular classes contribute only a lower-order correction to the projective point count; the leading term is not multiplied by the degree.

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

Above the square-degree cutoff the multiplicity correction has the O_n(d^2 p^(dimension-1/2)) scale required by CCDN Lemma 2.7.