Polynomial reconstruction controls exceptional points and finite point counts. The error is d times the reconstruction denominator's degree; a uniform O(d^2) bound requires a low-degree denominator.

theorem CCDN.projection_card_le_image_add {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] [Finite σ] [Finite τ] [DecidableEq (σ → K)] (I : Ideal (MvPolynomial τ K)) [I.IsPrime] (d : ℕ) (hdegree : HasFilteredCurveDegree I d) (a : σ → MvPolynomial τ K) (ha : ∀ (j : σ), (a j).totalDegree ≤ 1) (Q : MvPolynomial σ K) (P : τ → MvPolynomial σ K) (hQ : (MvPolynomial.aeval a) Q ∉ I) (hP : ∀ (i : τ), (MvPolynomial.aeval a) Q * MvPolynomial.X i - (MvPolynomial.aeval a) (P i) ∈ I) (S : Finset (τ → K)) (hS : ∀ z ∈ S, z ∈ idealZeroLocus I) : have π := fun (z : τ → K) (j : σ) => (MvPolynomial.eval z) (a j); S.card ≤ (Finset.image π S).card + d * Q.totalDegree

For every finite set of source points, projection loses at most d*deg(Q) points, where Q is any proper reconstruction denominator.