If a filtration is eventually generated one step at a time by a parameter, its linear growth has slope at most the function-field degree over K(t). Common denominators affect only the fixed additive offset in the bound.
Any finite family in a finite extension of K(t) fits in a bounded power block after multiplication by one nonzero rational-function denominator.
theorem
CCDN.parameter_recurrence_slope_le
{K : Type u_1}
{A : Type u_2}
{F : Type u_3}
[Field K]
[AddCommGroup A]
[Module K A]
[Field F]
[Algebra K F]
[Algebra (RatFunc K) F]
[IsScalarTower K (RatFunc K) F]
[Module.Finite (RatFunc K) F]
(V : ℕ → Submodule K A)
[∀ (n : ℕ), Module.Finite K ↥(V n)]
(L : A →ₗ[K] A)
(φ : A →ₗ[K] F)
(hφ : Function.Injective ⇑φ)
(hL : ∀ (x : A), φ (L x) = (algebraMap (RatFunc K) F) RatFunc.X * φ x)
(N : ℕ)
(hrec : ∀ n ≥ N, V (n + 1) = V n ⊔ Submodule.map L (V n))
(d : ℕ)
(hdegree : ∃ (M : ℕ) (c : ℤ), ∀ n ≥ M, ↑(Module.finrank K ↥(V n)) = ↑d * ↑n + c)
:
The Hilbert slope is at most the parameter extension degree whenever the coordinate filtration has the parameter-generation recurrence.