A projective curve with a proper standard chart reduces to a plane equation of the same degree. Projection loses at most d(d-1) affine points and at most d further points lie on the omitted hyperplane.

theorem CCDN.projective_curve_count_le_of_moment_projection {n d k₀ k₁ : ℕ} (I : Ideal (CoordinatePolynomial (n + 1))) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (hd : 0 < d) (hdegree : HasProjectiveCurveDegree I d) (f : MvPolynomial (Fin 2) ℚ) (hfd : f.totalDegree = d) (hk₀ : k₀ ≤ n ^ 2 * d) (hk₁ : k₁ ≤ n * d ^ 2) (hfI : (MvPolynomial.aeval ![momentCoordinate ℚ n k₀, momentCoordinate ℚ n k₁]) f ∈ projectiveChartIdeal I) (hcount : ∀ (S : Finset (Fin n → ℚ)), (∀ z ∈ S, ∀ g ∈ projectiveChartIdeal I, (MvPolynomial.eval z) g = 0) → S.card ≤ (Finset.image (fun (z : Fin n → ℚ) (i : Fin (Nat.succ 0).succ) => (MvPolynomial.eval z) (![momentCoordinate ℚ n k₀, momentCoordinate ℚ n k₁] i)) S).card + d * (d - 1)) (B : ℝ) (hB : 1 ≤ B) : projectiveCount (projectiveIdealZeroLocus I) B ≤ projectiveCount (projectiveZeroLocus (scaledHomogenize d 1 f)) (projectionBoxFactor n d * B) + d ^ 2

Let I be a prime ideal defining a projective curve of degree d not contained in the hyperplane X₀ = 0, and suppose the moment coordinates with parameters k₀ ≤ n ^ 2 * d and k₁ ≤ n * d ^ 2 satisfy the plane relation f of degree d on its affine chart, losing at most d * (d - 1) points on any finite set of chart points. Then the curve has at most d ^ 2 more rational points of height at most B than the projective plane curve defined by the homogenization of f has of height at most projectionBoxFactor n d * B.

theorem CCDN.exists_projective_plane_count_reduction {n d : ℕ} (I : Ideal (CoordinatePolynomial (n + 1))) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (hd : 0 < d) (hdegree : HasProjectiveCurveDegree I d) : ∃ (f : MvPolynomial (Fin 3) ℚ), f.IsHomogeneous d ∧ Irreducible f ∧ ∀ (B : ℝ), 1 ≤ B → projectiveCount (projectiveIdealZeroLocus I) B ≤ projectiveCount (projectiveZeroLocus f) (projectionBoxFactor n d * B) + d ^ 2

A projective curve of degree d > 0 in ℙⁿ, given by a prime ideal I not containing X 0, has at most d ^ 2 more rational points of height at most B than some irreducible projective plane curve of degree d has of height at most projectionBoxFactor n d * B.