Degree-one prime curves are affine lines

The eventual Hilbert-degree definition implies a one-dimensional increase in successive filtered spaces. Critical growth forces every coordinate to be affine in one transcendental coordinate, giving polynomial containment of an affine line.

theorem CCDN.degree_one_zeroLocus_eq_rationalAffineLine (p : Ideal (CoordinatePolynomial 3)) [p.IsPrime] (hp : p.height = 2) (hdegree : HasAffineCurveDegree p 1) (z : RatPoint 3) (hz : z ∈ idealZeroLocus p) : ∃ (v : RatPoint 3), v ≠ 0 ∧ idealZeroLocus p = rationalAffineLine z v ∧ ∀ f ∈ p, (MvPolynomial.aeval fun (k : Fin 3) => Polynomial.C (z k) + Polynomial.C (v k) * Polynomial.X) f = 0

A degree-one prime component with a rational point is exactly a rational affine line. This is equality of zero sets, not just containment.