Singular projective residue classes are counted in their selected affine charts. The correction is polynomial in the degree and does not change the leading finite-field point-count term.

theorem CCDN.projectivePlaneTotalMultiplicity_le_card_add_correction {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)) (hchar : d < p) : projectivePlaneTotalMultiplicity f hf ⋯ ≤ Fintype.card ↑(ProjectivePlaneResidue f p) + 3 * d ^ 2 * (d - 1)

The singular correction does not multiply the leading point-count term.