Projective finite-field points consist of the standard affine chart and at most d points at infinity. The infinity bound is proved by projective Bezout and introduces no extra leading multiple of p.

theorem CCDN.projectivePlaneResidue_card_le_affine_add_degree {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hproper : ¬(MvPolynomial.map (Int.castRingHom (ZMod p))) f ∣ MvPolynomial.X 0) : Fintype.card ↑(ProjectivePlaneResidue f p) ≤ Fintype.card (PlaneResidue ((affineChart 2) f) p) + d

The projective correction is at most d, preserving the leading p term in the already proved affine finite-field estimate.