Every positive-degree prime affine curve in characteristic zero admits an explicitly bounded integral linear plane projection preserving its degree. The first coordinate is constructed by infinity avoidance and the second by the quantitative primitive-element theorem.

Construct the rational-function field embedding from a transcendental coordinate, and prove the degree bound for the resulting field extension.

An infinity-avoiding linear form gives a degree-preserving plane projection. The parameter field and the second coordinate are constructed.

theorem CCDN.exists_bounded_degree_preserving_projection {K : Type u_1} [Field K] [CharZero K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] (d : ℕ) (hd : 0 < d) (hdegree : HasFilteredCurveDegree I d) : ∃ (k₀ : ℕ) (k₁ : ℕ) (f : MvPolynomial (Fin 2) K), k₀ ≤ n ^ 2 * d ∧ k₁ ≤ n * d ^ 2 ∧ Irreducible f ∧ f.totalDegree = d ∧ Transcendental K ((Ideal.Quotient.mk I) (momentCoordinate K n k₀)) ∧ ∀ (g : MvPolynomial (Fin (Nat.succ 0).succ) K), (MvPolynomial.aeval ![momentCoordinate K n k₀, momentCoordinate K n k₁]) g ∈ I ↔ f ∣ g

A bounded degree-preserving plane projection of a prime affine curve in characteristic zero. The curve need not be geometrically integral.

theorem CCDN.exists_bounded_projection_card_le {K : Type u_1} [Field K] [CharZero K] [DecidableEq (Fin 2 → K)] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] (d : ℕ) (hd : 0 < d) (hdegree : HasFilteredCurveDegree I d) : ∃ (k₀ : ℕ) (k₁ : ℕ) (f : MvPolynomial (Fin 2) K), k₀ ≤ n ^ 2 * d ∧ k₁ ≤ n * d ^ 2 ∧ Irreducible f ∧ f.totalDegree = d ∧ (∀ (g : MvPolynomial (Fin (Nat.succ 0).succ) K), (MvPolynomial.aeval ![momentCoordinate K n k₀, momentCoordinate K n k₁]) g ∈ I ↔ f ∣ g) ∧ ∀ (S : Finset (Fin n → K)), (∀ z ∈ S, z ∈ idealZeroLocus I) → S.card ≤ (Finset.image (fun (z : Fin n → K) => ![(MvPolynomial.eval z) (momentCoordinate K n k₀), (MvPolynomial.eval z) (momentCoordinate K n k₁)]) S).card + d * (d - 1)

An integral affine curve of degree d has a projection to the plane by two moment coordinates of bounded index whose image is cut out by an irreducible equation of degree d, and which identifies at most d(d-1) points of any finite subset of the curve.