The plane curve estimate gives a smaller degree exponent for curves specified by their filtered Hilbert polynomial. The construction of the finite birational projection and its integer matrix is internal.
theorem
CCDN.projective_hilbert_curve_dimension_growth
(n : ℕ)
(hn : 1 ≤ n)
:
∃ (C : ℝ),
0 < C ∧ ∀ (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)),
I.IsPrime →
IsHomogeneousIdeal I →
∀ (d : ℕ),
5 ≤ d →
HasProjectiveDimensionDegree I 1 d →
∀ (B : ℝ), 1 ≤ B → ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ C * ↑d ^ (3 * (n + 1) + 4) * B
Dimension growth for projective curves in ℙⁿ over ℚ, specified by their Hilbert
polynomial: there is a constant C > 0, depending only on n ≥ 1, such that every homogeneous
prime ideal I of projective dimension 1 and degree d ≥ 5 has at most
C * d ^ (3 * (n + 1) + 4) * B rational points of height at most B for all B ≥ 1.