Birkhoff renormalization of the Minimal-Yield character (MCB Prop. 3.5.6)

[MCB25] §3.5.2.2

The payoff of MCB §3.5.2, instantiating the framework-agnostic Birkhoff-renormalization machinery of Core/Algebra/RootedTree/BirkhoffLaurent.lean at the Minimal-Yield character ϕt = gradingChar.

By Lemma 3.5.5, ϕt is entirely nonpolar; in the Birkhoff language this means birkhoffMinusTree(ϕt) = 0 — there is no divergence to subtract, so ϕt is its own renormalization. This is exactly why ϕt cannot separate Internal/External from Sideward Merge: one must instead use the intermediate-derivation character ψt (Cor. 3.5.4, eq. 3.5.7), whose nontrivial polar part the full Birkhoff factorization — not plain 1 − R, since R is a Rota–Baxter operator and not an algebra homomorphism — eliminates (Prop. 3.5.6). The renormalized part always lands in the nonpolar subring DM[[t]] (polarHahn_birkhoffPlus_of', in Core); for ψt that is where the polar Sideward content is removed. Building ψt (a sum over all intermediate derivation pairs (F, F')) is left to future work.

Main results

• birkhoffMinusTree_gradingChar: ϕt is trivially renormalized (Lemma 3.5.5, Birkhoff form).
• renormGradingChar: the renormalized Minimal-Yield character ϕt,+.

References

[MCB25] (Prop. 3.5.3, Lemma 3.5.5, Prop. 3.5.6)

ϕt is trivially renormalized (MCB Lemma 3.5.5, Birkhoff form)

theorem Minimalist.Merge.birkhoffMinusTree_gradingChar {α : Type u_1} {R : Type u_2} [CommRing R] (T : RootedTree.Nonplanar α) : RootedTree.ConnesKreimer.birkhoffMinusTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T = 0

ϕt is its own renormalization (MCB Lemma 3.5.5 in Birkhoff form): the Bogolyubov negative part of the Minimal-Yield character ϕt = gradingChar vanishes on every tree, because ϕt is nonpolar (polarHahn_gradingChar_ofTree). There is no divergence to subtract — which is why ϕt cannot detect Sideward Merge.

The renormalized character

noncomputable def Minimalist.Merge.renormGradingChar {α : Type u_1} {R : Type u_2} [CommRing R] : RootedTree.ConnesKreimer R (RootedTree.Nonplanar α) →ₐ[R] LaurentSeries R

The renormalized Minimal-Yield character ϕt,+ = (1−R)ϕ̃t = birkhoffPlus(ϕt).

Equations

• Minimalist.Merge.renormGradingChar = RootedTree.ConnesKreimer.birkhoffPlus Minimalist.Merge.gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar

theorem Minimalist.Merge.birkhoffPlusTree_gradingChar {α : Type u_1} {R : Type u_2} [CommRing R] (T : RootedTree.Nonplanar α) : RootedTree.ConnesKreimer.birkhoffPlusTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T = RootedTree.ConnesKreimer.birkhoffPrepTree gradingChar.toLinearMap LaurentSeries.rotaBaxterPolar T

ϕt,+ = ϕ̃t on every tree: since ϕt carries no divergence (birkhoffMinusTree_gradingChar), the renormalized part of ϕt equals its Bogolyubov preparation — nothing is subtracted. The Birkhoff factorization does no work on ϕt, the concrete form of MCB Lemma 3.5.5.