The zero-dimensional case of projective dimension growth. A one-parameter normalization sends every projective point to the unique point of projective zero-space; its affine fiber bound controls the whole source, independently of height.

theorem CCDN.zero_dimensional_projective_count_le {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) [I.IsPrime] (d : ℕ) (hdim : (filteredHilbertPolynomial I).natDegree = 1) (hdegree : (filteredHilbertPolynomial I).leadingCoeff = ↑d) (B : ℝ) : projectiveCount (projectiveIdealZeroLocus I) B ≤ d ^ (n + 1)

If a prime ideal I in n + 1 variables has Hilbert dimension one (projective dimension zero) and degree d, its projective zero locus has at most d ^ (n + 1) rational points of any height.