Once a linear parameter generates the degree filtration, a bounded moment coordinate produces a degree-preserving plane equation. This combines full function-field degree with the quantitative primitive-element theorem.

Eventual generation of the affine degree filtration by a linear parameter forces the function-field extension to have the full Hilbert degree.

theorem CCDN.exists_full_degree_primitive_projection {K : Type u_1} {F : Type u_2} [Field K] [CharZero K] [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] [Algebra (MvPolynomial (Fin n) K ⧸ I) F] [IsScalarTower K (MvPolynomial (Fin n) K ⧸ I) F] [IsFractionRing (MvPolynomial (Fin n) K ⧸ I) F] (d : ℕ) (hdegree : HasFilteredCurveDegree I d) (l : MvPolynomial (Fin n) K) (hl : l.totalDegree ≤ 1) (he : (algebraMap (MvPolynomial (Fin n) K ⧸ I) F) ((Ideal.Quotient.mk I) l) = (algebraMap (RatFunc K) F) RatFunc.X) (N : ℕ) (hrec : ∀ m ≥ N, filteredCoordinateSpace I (m + 1) = filteredCoordinateSpace I m ⊔ Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk I) l)) (filteredCoordinateSpace I m)) : ∃ (k : ℕ) (f : MvPolynomial (Fin 2) K), k ≤ n * d ^ 2 ∧ Irreducible f ∧ f.totalDegree = d ∧ ∀ (g : MvPolynomial (Fin (Nat.succ 0).succ) K), (MvPolynomial.aeval ![l, momentCoordinate K n k]) g ∈ I ↔ f ∣ g

Build the bounded second projection coordinate and a plane equation of exactly degree d from a parameter satisfying eventual filtered generation.