Birkhoff renormalization of Laurent-series characters [UPSTREAM]

The Birkhoff factorization (BirkhoffFactorization.lean) of a character φ : H → A⸨X⸩ from the Connes–Kreimer Hopf algebra of nonplanar rooted forests into a ring of Laurent series, with respect to the polar-part Rota–Baxter operator rotaBaxterPolar (RotaBaxterLaurent.lean) — the minimal-subtraction scheme of Connes–Kreimer renormalization. Two framework-agnostic facts:

• the renormalized part φ₊ = (1−R)φ̃ always lands in the nonpolar subring A[[t]], since 1−R projects onto it (polarHahn_birkhoffPlusTree, polarHahn_birkhoffPlus_of');
• a character that is already nonpolar on every tree has a trivial negative part φ₋ = 0 (birkhoffMinusTree_eq_zero_of_nonpolar) — no divergence to subtract.

These are the algebraic core of [MCB25]'s "Minimal Yield as Birkhoff factorization" (§3.5.2); the syntactic interpretation (the Minimal-Yield character and its grading) lives downstream in Syntax/Minimalist/Merge/.

Main results

• birkhoffMinusTree_eq_zero_of_nonpolar: a nonpolar character has trivial Bogolyubov negative part.
• polarHahn_birkhoffPlusTree / polarHahn_birkhoffPlus_of': the renormalized part is nonpolar.

References

[MCB25] (§3.5.2, Prop. 3.1.7, Prop. 3.5.6)

A nonpolar character has trivial Bogolyubov negative part

theorem RootedTree.ConnesKreimer.birkhoffMinusTree_eq_zero_of_nonpolar {R : Type u_1} [CommRing R] {α : Type u_2} (φ : ConnesKreimer R (Nonplanar α) →ₐ[R] LaurentSeries R) (hφ : ∀ (T : Nonplanar α), (φ (ofTree T)).polarHahn = 0) (T : Nonplanar α) : birkhoffMinusTree φ.toLinearMap LaurentSeries.rotaBaxterPolar T = 0

If a character φ is nonpolar on every tree (R·φ(ofTree T) = 0), its Bogolyubov negative part under the polar-projection Rota–Baxter operator vanishes: φ₋(T) = 0. By strong recursion on T.depth: every nontrivial cut's pruned forest contains a subtree of smaller depth, where φ₋ is 0 by the recursive hypothesis — killing that term — and the trivial cut contributes the nonpolar trunk value φ(ofTree …), so R annihilates the whole Bogolyubov preparation.

The renormalized part always lands in the nonpolar subring

theorem RootedTree.ConnesKreimer.polarHahn_birkhoffPlusTree {R : Type u_1} [CommRing R] {α : Type u_2} (φ : ConnesKreimer R (Nonplanar α) →ₐ[R] LaurentSeries R) (T : Nonplanar α) : (birkhoffPlusTree φ.toLinearMap LaurentSeries.rotaBaxterPolar T).polarHahn = 0

The renormalized character lands in A[[t]] ([MCB25] Prop. 3.5.6's ψt,+ : H → DM[[t]]): for any character φ, the renormalized part φ₊(T) = (1−R)(φ̃(T)) is nonpolar — R·φ₊(T) = 0 — because R is idempotent, so φ₊ is in the range of 1 − R.

theorem RootedTree.ConnesKreimer.polarHahn_birkhoffPlus_of' {R : Type u_1} [CommRing R] {α : Type u_2} (φ : ConnesKreimer R (Nonplanar α) →ₐ[R] LaurentSeries R) (F : Forest (Nonplanar α)) : ((birkhoffPlus φ.toLinearMap LaurentSeries.rotaBaxterPolar) (of' F)).polarHahn = 0

φ₊ : H → A[[t]] on every workspace (Prop. 3.5.6, forest level): the renormalized character is nonpolar on each forest basis element, being the product of the nonpolar per-tree renormalized parts (the nonpolar series form a subalgebra).