Positive Hilbert growth forces any parameter generating the eventual filtration recurrence to be transcendental.
theorem
CCDN.recurrence_parameter_transcendental
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Finite σ]
(I : Ideal (MvPolynomial σ K))
(d : ℕ)
(hd : 0 < d)
(hdegree : HasFilteredCurveDegree I d)
(l : MvPolynomial σ K)
(N : ℕ)
(hrec :
∀ m ≥ N,
filteredCoordinateSpace I (m + 1) = filteredCoordinateSpace I m ⊔
Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk I) l)) (filteredCoordinateSpace I m))
:
Transcendental K ((Ideal.Quotient.mk I) l)
A parameter giving eventual filtered generation on a positive-degree curve cannot satisfy a polynomial over the ground field.