A degree-preserving linear plane projection of a prime affine curve in characteristic zero loses at most d(d-1) points from any finite source set. The proof constructs a common derivative denominator and all reconstruction identities, with no normalization or exceptional-fiber hypothesis.

theorem CCDN.degree_preserving_projection_reconstruction {K : Type u_1} {τ : Type u_2} [Field K] [CharZero K] [Finite τ] (I : Ideal (MvPolynomial τ K)) [I.IsPrime] (a : Fin 2 → MvPolynomial τ K) (ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1) (d : ℕ) (hdegree : HasFilteredCurveDegree I d) (hu : Transcendental K ((Ideal.Quotient.mk I) (a 0))) (f : MvPolynomial (Fin 2) K) (hf : f ≠ 0) (hfd : f.totalDegree = d) (hker : ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g) : (MvPolynomial.aeval a) ((MvPolynomial.pderiv 1) f) ∉ I ∧ ((MvPolynomial.pderiv 1) f).totalDegree ≤ d - 1 ∧ ∃ (P : τ → MvPolynomial (Fin 2) K), ∀ (i : τ), (P i).totalDegree ≤ d ∧ (MvPolynomial.aeval a) ((MvPolynomial.pderiv 1) f) * MvPolynomial.X i - (MvPolynomial.aeval a) (P i) ∈ I

All source coordinates have the same proper reconstruction denominator, namely the partial derivative of the plane image equation.

theorem CCDN.degree_preserving_projection_card_le {K : Type u_1} {τ : Type u_2} [Field K] [CharZero K] [Finite τ] [DecidableEq (Fin 2 → K)] (I : Ideal (MvPolynomial τ K)) [I.IsPrime] (a : Fin 2 → MvPolynomial τ K) (ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1) (d : ℕ) (hdegree : HasFilteredCurveDegree I d) (hu : Transcendental K ((Ideal.Quotient.mk I) (a 0))) (f : MvPolynomial (Fin 2) K) (hf : f ≠ 0) (hfd : f.totalDegree = d) (hker : ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g) (S : Finset (τ → K)) (hS : ∀ z ∈ S, z ∈ idealZeroLocus I) : S.card ≤ (Finset.image (fun (z : τ → K) (j : Fin 2) => (MvPolynomial.eval z) (a j)) S).card + d * (d - 1)

Uniform exceptional-fiber control for any degree-preserving linear plane projection, including curves that are not geometrically integral.