The exact relation between a homogeneous affine cone and its projective zero locus. The origin is counted once and each projective zero contributes exactly one nonzero vector for every unit in the field.

theorem CCDN.homogeneous_projective_count_of_cone_bound {K : Type u_1} [Field K] [Fintype K] {n d : ℕ} (f : MvPolynomial (Fin (n + 3)) K) (hf : f.IsHomogeneous d) (hd : 0 < d) {H : ℝ} (hH : 0 ≤ H) (hcone : ↑(Nat.card { v : Fin (n + 3) → K // (MvPolynomial.eval v) f = 0 }) ≤ ↑(Fintype.card K) ^ (n + 2) + H * ↑(Fintype.card K) ^ (n + 1)) : ↑(Nat.card ↑(projectiveZeroLocus f)) ≤ ↑(Fintype.card K) ^ (n + 1) + 2 * (H + 1) * ↑(Fintype.card K) ^ n

Passing from the affine cone to its projective zero locus preserves the leading coefficient one, with an explicit lower-order error.