Construct a polynomial family of plane relations for linear projections of a prime affine curve. The relation has degree at most the curve's Hilbert degree and remains nonzero at parameter zero.

theorem CCDN.exists_curve_projection_relation_family {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))) (l : MvPolynomial τ K) (hl : l.totalDegree ≤ 1) : let V := MvPolynomial.restrictTotalDegree (Fin 2) K d; have b := Module.finBasis K ↥V; ∃ (v : Fin (Module.finrank K ↥V) → Polynomial K), ∑ j : Fin (Module.finrank K ↥V), Polynomial.map (algebraMap K (MvPolynomial τ K ⧸ I)) (v j) * (planeLinearDeformation (fun (i : Fin 2) => (Ideal.Quotient.mk I) (a i)) 1 ((Ideal.Quotient.mk I) l)) ↑(b j) = 0 ∧ ∃ (j : Fin (Module.finrank K ↥V)), Polynomial.eval 0 (v j) ≠ 0

Every bounded-degree linear displacement has a nonzero plane relation. The relations can be chosen polynomially in the displacement parameter and with a nonzero specialization at zero.