Minimal Yield in the Laurent-series ring

Minimal Yield can be restated as a Birkhoff factorization in the ring of Laurent series DM[t⁻¹][[t]] over the algebra of free Merge derivations, weighting a transformation F → F' by tᵟ for a grading δ read off the size measures. This file defines the gradings

δb₀ F F' = b₀ F − b₀ F', δα F F' = α F' − α F, δσ F F' = σ F' − σ F,

shows Minimal Yield is 0 ≤ δb₀ ∧ 0 ≤ δα ∧ δσ = 1, and connects the gradings to the polar-part operator R = LaurentSeries.polarHahn: a transformation satisfies weak Minimal Yield iff its δb₀- and δα-monomials are both nonpolar (weak_iff_polarHahn).

The character ϕt : H →ₐ[R] LaurentSeries R on the Hopf algebra of nonplanar forests records, in place of the derivation coefficients of DM, only the grading tᵟ with δ = δα; on a forest it is t^{α(F)}. Since α(F) ≥ 0 it is nonpolar on every forest, so its Bogolyubov negative part vanishes and it is its own renormalization: ϕt cannot see Sideward Merge, which is why the intermediate-derivation character ψt is needed. Summing monomials over a family of transformations, as ψt does, the polar part is the sum over the divergent ones (LaurentSeries.polarHahn_sum_map_single).

Main definitions

• Minimalist.MinimalYield.δb₀, δα, δσ: the signed gradings.
• Minimalist.MinimalYield.gradingChar: the character ϕt.
• Minimalist.MinimalYield.renormGradingChar: its Birkhoff-renormalized part ϕt,+.

Main results

• Minimalist.MinimalYield.iff_gradings, weak_iff_polarHahn: Minimal Yield as sign conditions and as nonpolarity.
• Minimalist.MinimalYield.polarHahn_gradingChar_of': ϕt is nonpolar.
• Minimalist.MinimalYield.birkhoffMinusTree_gradingChar: its negative part vanishes.

References

• [marcolli-chomsky-berwick-2025], §3.5.2 (Propositions 3.5.2, 3.5.3, 3.5.6, Corollary 3.5.4, Lemma 3.5.5)

The gradings

def Minimalist.MinimalYield.δb₀ {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δb₀ F F' = b₀ F − b₀ F', nonnegative iff F → F' does not diverge.

Equations

• Minimalist.MinimalYield.δb₀ F F' = ↑(Multiset.card F) - ↑(Multiset.card F')

def Minimalist.MinimalYield.δα {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δα F F' = α F' − α F, nonnegative iff F → F' loses no information.

Equations

• Minimalist.MinimalYield.δα F F' = ↑(Forest.numEdges F') - ↑(Forest.numEdges F)

def Minimalist.MinimalYield.δσ {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δσ F F' = σ F' − σ F, equal to 1 iff F → F' has minimal yield.

Equations

• Minimalist.MinimalYield.δσ F F' = ↑(Forest.numNodes F') - ↑(Forest.numNodes F)

theorem Minimalist.MinimalYield.δσ_eq {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : δσ F F' = δα F F' - δb₀ F F'

theorem Minimalist.MinimalYield.weak_iff_gradings {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : MinimalYieldWeak F F' ↔ 0 ≤ δb₀ F F' ∧ 0 ≤ δα F F'

theorem Minimalist.MinimalYield.iff_gradings {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : MinimalYield F F' ↔ 0 ≤ δb₀ F F' ∧ 0 ≤ δα F F' ∧ δσ F F' = 1

theorem Minimalist.MinimalYield.weak_iff_polarHahn {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) [Nontrivial R] : MinimalYieldWeak F F' ↔ LaurentSeries.polarHahn ((HahnSeries.single (δb₀ F F')) 1) = 0 ∧ LaurentSeries.polarHahn ((HahnSeries.single (δα F F')) 1) = 0

Weak Minimal Yield holds iff the δb₀- and δα-monomials of F → F' are both nonpolar.

The character ϕt

noncomputable def Minimalist.MinimalYield.gradingMonomialTree {α : Type u_1} {R : Type u_3} [CommRing R] (T : UnorderedTree α) : LaurentSeries R

The value of ϕt on a tree: t^{α(T)}.

Equations

• Minimalist.MinimalYield.gradingMonomialTree T = (HahnSeries.single ↑T.numEdges) 1

noncomputable def Minimalist.MinimalYield.gradingMonoidHom {α : Type u_1} {R : Type u_3} [CommRing R] : Multiplicative (UnorderedTree.Forest (UnorderedTree α)) →* LaurentSeries R

ϕt on forests, multiplicative over disjoint union.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Minimalist.MinimalYield.gradingChar {α : Type u_1} {R : Type u_3} [CommRing R] : ConnesKreimer R (UnorderedTree α) →ₐ[R] LaurentSeries R

The character ϕt : H →ₐ[R] LaurentSeries R, ϕt(F) = t^{α(F)}.

Equations

• Minimalist.MinimalYield.gradingChar = ConnesKreimer.lift Minimalist.MinimalYield.gradingMonoidHom

@[simp]

theorem Minimalist.MinimalYield.gradingChar_apply_of' {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : gradingChar (ConnesKreimer.of' F) = (Multiset.map gradingMonomialTree F).prod

theorem Minimalist.MinimalYield.prod_gradingMonomialTree {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : (Multiset.map gradingMonomialTree F).prod = (HahnSeries.single ↑(Forest.numEdges F)) 1

ϕt(F) = t^{α(F)}, since α is additive over forests.

theorem Minimalist.MinimalYield.gradingChar_apply_of'_eq {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : gradingChar (ConnesKreimer.of' F) = (HahnSeries.single ↑(Forest.numEdges F)) 1

@[simp]

theorem Minimalist.MinimalYield.gradingChar_apply_ofTree {α : Type u_1} {R : Type u_3} [CommRing R] (T : UnorderedTree α) : gradingChar (ConnesKreimer.ofTree T) = (HahnSeries.single ↑T.numEdges) 1

ϕt is nonpolar

theorem Minimalist.MinimalYield.polarHahn_gradingChar_of' {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : (gradingChar (ConnesKreimer.of' F)).polarHahn = 0

ϕt is nonpolar on every forest, since α(F) ≥ 0.

theorem Minimalist.MinimalYield.polarHahn_gradingChar_ofTree {α : Type u_1} {R : Type u_3} [CommRing R] (T : UnorderedTree α) : (gradingChar (ConnesKreimer.ofTree T)).polarHahn = 0

Birkhoff renormalization

theorem Minimalist.MinimalYield.birkhoffMinusTree_gradingChar {α : Type u_1} {R : Type u_3} [CommRing R] (T : UnorderedTree α) : ConnesKreimer.birkhoffMinusTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T = 0

The Bogolyubov negative part of ϕt vanishes on every tree.

noncomputable def Minimalist.MinimalYield.renormGradingChar {α : Type u_1} {R : Type u_3} [CommRing R] : ConnesKreimer R (UnorderedTree α) →ₐ[R] LaurentSeries R

The renormalized character ϕt,+ = birkhoffPlus ϕt.

Equations

• Minimalist.MinimalYield.renormGradingChar = ConnesKreimer.birkhoffPlus Minimalist.MinimalYield.gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar

theorem Minimalist.MinimalYield.birkhoffPlusTree_gradingChar {α : Type u_1} {R : Type u_3} [CommRing R] (T : UnorderedTree α) : ConnesKreimer.birkhoffPlusTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T = ConnesKreimer.birkhoffPrepTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T

ϕt,+ coincides with the Bogolyubov preparation of ϕt on every tree.