The projective curve count of Theorem 2 with an explicit constant. In a chart where the curve is not contained in the hyperplane at infinity, a bounded projection to the plane and the projective plane count give the bound (projective_curve_count_of_proper_chart); a coordinate permutation, which costs no height, chooses such a chart (projective_curve_count).

noncomputable def CCDN.projectiveCurveConstant (n : ℕ) : ℝ

The explicit constant projectivePlaneAbsoluteConstant * exp (2 * projectionLogConstant n) + 1 of the projective curve count in ℙⁿ: the plane-curve constant, enlarged by the height loss of a bounded projection to the plane, plus one to absorb the d² error term of the projection.

Equations

• CCDN.projectiveCurveConstant n = CCDN.projectivePlaneAbsoluteConstant * Real.exp (2 * CCDN.projectionLogConstant n) + 1

theorem CCDN.projectiveCurveConstant_pos (n : ℕ) : 0 < projectiveCurveConstant n

The constant projectiveCurveConstant n is positive.

theorem CCDN.projective_curve_count_of_proper_chart {n d : ℕ} (I : Ideal (CoordinatePolynomial (n + 1))) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (hd : 0 < d) (hdegree : HasProjectiveCurveDegree I d) {B : ℝ} (hB : 1 ≤ B) : ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ projectiveCurveConstant n * projectiveCurveEstimate d B

Let I be the homogeneous prime ideal of a projective curve of degree d > 0 in ℙⁿ that is not contained in the hyperplane X 0 = 0 (that is, X 0 ∉ I). For B ≥ 1, the number of rational points of height at most B on the curve is at most projectiveCurveConstant n * d⁴ B^(2/d).

theorem CCDN.projective_curve_count {n d : ℕ} (I : Ideal (CoordinatePolynomial (n + 1))) [I.IsPrime] (hd : 0 < d) (hdegree : HasProjectiveCurveDegree I d) {B : ℝ} (hB : 1 ≤ B) : ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ projectiveCurveConstant n * projectiveCurveEstimate d B

Let I be the homogeneous prime ideal of a projective curve of degree d > 0 in ℙⁿ. For B ≥ 1, the number of rational points of height at most B on the curve is at most projectiveCurveConstant n * d⁴ B^(2/d).