Global cofactors from local data of fixed rank

Consider a nonpositive Hahn series whose translated truncation at every nonpositive cutoff, including zero, has degree at most β. Its exact rank-β cutoffs accumulate nowhere. Suppose a finite family of homogeneous lifts is given, each with a degree bound and strictly smaller proper translated truncations, and at every exact rank-β cutoff local cofactors are prescribed that correct the truncation below degree β. Interpolating those local cofactors produces global cofactors with the same pointwise degree bounds, whose combination with the lifts corrects the series below degree β at every nonpositive cutoff simultaneously. The subtracted term is an exact finite combination of the lifts, so this step preserves membership in the ideal they generate.

theorem HahnSeries.Nonpositive.exists_forall_degree_translatedTruncLE_sub_sum_mul_lt {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [CommRing R] [NoZeroDivisors R] [CharZero R] (β : NatOrdinal) {ι : Type w} [Fintype ι] (V : ι → Nonpositive G R) (ρ σ : ι → NatOrdinal) (hgrade : ∀ (j : ι), ρ j + σ j ≤ β) (hV : ∀ (j : ι), cantorBendixsonDegreeValuation.toFun (V j) ≤ ↑(σ j)) (hVcut : ∀ (j : ι), ∀ x < 0, cantorBendixsonDegreeValuation.toFun ((translatedTruncLE x) (V j)) < ↑(σ j)) (u : Nonpositive G R) (hu : ∀ x ≤ 0, cantorBendixsonDegreeValuation.toFun ((translatedTruncLE x) u) ≤ ↑β) (w : { x : G // x ∈ (↑u).closedSupport ∧ (↑u).closedSupport.cantorBendixsonRank ⋯ x = NatOrdinal.val β } → ι → Nonpositive G R) (hw : ∀ (i : { x : G // x ∈ (↑u).closedSupport ∧ (↑u).closedSupport.cantorBendixsonRank ⋯ x = NatOrdinal.val β }) (j : ι), cantorBendixsonDegreeValuation.toFun (w i j) ≤ ↑(ρ j)) (hcorr : ∀ (i : { x : G // x ∈ (↑u).closedSupport ∧ (↑u).closedSupport.cantorBendixsonRank ⋯ x = NatOrdinal.val β }), cantorBendixsonDegreeValuation.toFun ((translatedTruncLE ↑i) u - ∑ j : ι, w i j * V j) < ↑β) : ∃ (c : ι → Nonpositive G R), (∀ (j : ι), ∀ x ≤ 0, cantorBendixsonDegreeValuation.toFun ((translatedTruncLE x) (c j)) ≤ ↑(ρ j)) ∧ ∀ x ≤ 0, cantorBendixsonDegreeValuation.toFun ((translatedTruncLE x) (u - ∑ j : ι, c j * V j)) < ↑β

Local cofactors at every exact top-rank cutoff interpolate to global cofactors. They keep the prescribed pointwise degree bounds, and subtracting their products with the generators leaves a series whose translated truncations have degree strictly below β at every nonpositive cutoff, including zero.