Reduce the integral-point count of an arbitrary prime affine curve to the proved plane count, using the constructed degree-preserving projection.

theorem CCDN.rationalPoint_injective (n : ℕ) : Function.Injective rationalPoint

The inclusion of integer points into rational points is injective.

theorem CCDN.affine_curve_count_le_of_moment_projection {n d k₀ k₁ : ℕ} (I : Ideal (CoordinatePolynomial n)) (f : MvPolynomial (Fin 2) ℚ) (hk₀ : k₀ ≤ n ^ 2 * d) (hk₁ : k₁ ≤ n * d ^ 2) (hker : ∀ (g : MvPolynomial (Fin (Nat.succ 0).succ) ℚ), (MvPolynomial.aeval ![momentCoordinate ℚ n k₀, momentCoordinate ℚ n k₁]) g ∈ I ↔ f ∣ g) (hcount : ∀ (S : Finset (Fin n → ℚ)), (∀ z ∈ S, z ∈ idealZeroLocus I) → 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) : count (idealZeroLocus I) B ≤ count (zeroLocus f) (projectionBoxFactor n d * B) + d * (d - 1)

Suppose the projection of the affine variety of I by the moment coordinates k₀, k₁ has kernel generated by the plane polynomial f, and that this projection loses at most d * (d - 1) points on any finite set of rational points of the variety. Then the integral points of height at most B on the variety number at most those of height projectionBoxFactor n d * B on the plane curve f = 0, plus d * (d - 1).

theorem CCDN.exists_plane_count_reduction {n : ℕ} (I : Ideal (CoordinatePolynomial n)) [I.IsPrime] (d : ℕ) (hd : 0 < d) (hdegree : HasAffineCurveDegree I d) : ∃ (f : MvPolynomial (Fin 2) ℚ), Irreducible f ∧ f.totalDegree = d ∧ ∀ (B : ℝ), 1 ≤ B → count (idealZeroLocus I) B ≤ count (zeroLocus f) (projectionBoxFactor n d * B) + d * (d - 1)

An integral affine curve of degree d has an irreducible plane equation f of degree d such that, for every radius B ≥ 1, its integral points of height at most B number at most those of f in a box enlarged by projectionBoxFactor n d, plus d(d-1).