Linear occurrence of a maximal variable #
The differentiated truncation expansion makes all sufficiently high components of the maximal partial derivative vanish. If that variable occurred at least twice, ordinal separation would put the cutoff strictly below the derivative's degree. A sufficiently late translated truncation then has degree above the cutoff, contradicting the vanishing.
theorem
HahnSeries.Germ.LimitOrdinalRelationAtCutoff.degreeOf_eq_one
{G : Type u}
{K : Type v}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[UniformSpace G]
[IsUniformAddGroup G]
[OrderTopology G]
[Nontrivial G]
[CompleteSpace G]
[Field K]
[CharZero K]
{ι : Type w}
{wt : ι → NatOrdinal}
{xg : ι → Nonpositive.cantorBendixsonDegreeValuation.AssociatedGraded}
{σ : Nonpositive.LiftFamily wt xg}
{α : NatOrdinal}
(S : LimitOrdinalRelationAtCutoff σ α)
(hx : OrdinalGraded.IsMinimalSystem (DirectSum.rangeLof K Nonpositive.cantorBendixsonDegreeValuation.Component) wt xg)
(hσ : σ.HasLowerTruncationDegrees)
(hinj : ∀ β < α, OrdinalGraded.InjectiveAt K wt xg β)
:
Under the cutoff bounds used when the degree is a limit ordinal, a maximal variable occurs linearly.