The translated truncations of a term u · q(b_𝓑) satisfy (p)

Let q ∈ K[X] be homogeneous of degree c, evaluated at principal-series representatives, and let u be a series of ordinal value below ω^(b+1) whose translated truncations at cutoffs ζ < 0 have ordinal value below ω^b (for instance a principal series of degree b), with b ⊕ c < α. The separation condition (n) for (b, c, τ) — b ⊕ θ < τ for every θ < c — gives, for every cutoff ζ ≤ 0, that pol((u q(b_𝓑))^{|ζ})_{≥τ} lies in the ideal (q): the translated truncations of u · q(b_𝓑) satisfy the condition (p) for (q; τ). By the convolution formula, read in polynomials [Ber00, Lem. 7.5], pol((u q(b_𝓑))^{|ζ}) = pol(u^{|ζ}) · q + ∑ pol(u^{|β}) pol(q(b_𝓑)^{|ζ - β}), the first term lies in (q) and every other term has as a factor the polynomial of a translated truncation of q(b_𝓑) at a cutoff < 0, hence has degree below τ.

theorem Berarducci.Lifts.componentsGE_pol_translatedTruncation_mul_aeval_mem {K : Type v} [Field K] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → PrincipalSubring K} (σ : Lifts wt x) (hx : OrdinalGraded.IsMinimalSystem (principalGrading K) wt x) {α : NatOrdinal} (hinj : ∀ β < α, OrdinalGraded.InjectiveAt K wt x β) (hσ : σ.IsPrincipal) {q : MvPolynomial ι K} {c : NatOrdinal} (hq : MvPolynomial.IsWeightedHomogeneous wt q c) {u : Series K} {b : NatOrdinal} (hu : ordinalValue u < ω^ (b + 1)) (hucut : ∀ ζ < 0, ordinalValue (translatedTruncation (↑u) ζ) < ω^ b) (hbc : b + c < α) {τ : NatOrdinal} (hsep : ∀ θ < c, b + θ < τ) {ζ : ℝ} (hζ : ζ ≤ 0) : MvPolynomial.componentsGE wt τ (σ.pol hx α (translatedTruncation (↑(u * (MvPolynomial.aeval σ.lift) q)) ζ)) ∈ Ideal.span (Set.range fun (x : Unit) => q)

High-degree components of translated truncations of a polynomial multiple. Under the displayed ordinal-value and Hessenberg-sum bounds, the components of degree at least τ of pol((u * q(b_𝓑))^{|ζ}) lie in the principal ideal generated by q.