Dimension growth for homogeneous prime ideals of positive projective dimension.

theorem CCDN.projective_variety_dimension_growth (m k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (I : Ideal (MvPolynomial (Fin (m + k + 2)) ℚ)), I.IsPrime → IsHomogeneousIdeal I → ∀ (d : ℕ), 5 ≤ d → HasProjectiveDimensionDegree I (m + 1) d → ∀ (B : ℝ), 1 ≤ B → ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ C * ↑d ^ projectionDegreeExponent m k * B ^ (m + 1)

The general projective-variety bound, with dimension and codimension displayed separately. The hypotheses use the Hilbert polynomial of the coordinate ring.