The δ-grading of Minimal Yield and the polar part (MCB §3.5.2.1)

[MCB25] §3.5.2.1, book p. 267

MCB's §3.5.2 recasts Minimal Yield (Def. 1.6.1) as a Birkhoff factorization in a ring of Laurent series DM[t⁻¹][[t]] with coefficients in the algebra of free Merge derivations, weighting each derivation F → F' by tᵟ for a grading δ ∈ {δb₀, δα, δσ}. This file is the grading layer between MinimalYield.lean's size measures b₀/α/σ and the polar-part Rota–Baxter operator LaurentSeries.polarHahn of RotaBaxterLaurent.lean (MCB Prop. 3.5.2).

The signed deltas (MCB §3.5.2.1) of a transformation F → F':

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

with σ = b₀ + α giving δσ = δα − δb₀. Minimal Yield (Def. 1.6.1) is exactly δb₀ ≥ 0 ∧ δα ≥ 0 ∧ δσ = 1 (no divergence / no information loss / minimality of yield).

The bridge to the polar projection: a derivation graded tᵟ lands in the polar part (δ < 0, fixed by R = polarHahn, the divergent part Birkhoff factorization removes) iff its grading is negative. Minimal-Yield-respecting steps (External/Internal Merge) have δ ≥ 0, hence nonpolar (the per-merge shadow of MCB Lemma 3.5.5); the divergent Sideward Merge steps 3(a)/3(b) have δb₀ = −1 < 0, hence polar — the derivations MCB Prop. 3.5.6's factorization eliminates.

Main definitions

• Minimalist.Merge.δb₀ / δα / δσ: the signed ℤ-valued gradings.
• Minimalist.Merge.gradeMonomial: the Laurent monomial tᵈ whose polarity tracks d.

References

[MCB25] (§3.5.2.1, Prop. 3.5.2, Lemma 3.5.5, Prop. 3.5.6)

The δ-grading (MCB §3.5.2.1)

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

δb₀ = b₀ F − b₀ F' (MCB §3.5.2.1): divergence; ≥ 0 is "no divergence".

Equations

• Minimalist.Merge.δb₀ F F' = ↑(RootedTree.Forest.b₀ F) - ↑(RootedTree.Forest.b₀ F')

def Minimalist.Merge.δα {α : Type u_1} {β : Type u_2} (F F' : RootedTree.Forest (RootedTree.Nonplanar (α ⊕ β))) : ℤ

δα = α F' − α F (MCB §3.5.2.1): information gain; ≥ 0 is "no information loss".

Equations

• Minimalist.Merge.δα F F' = ↑(RootedTree.Forest.alpha F') - ↑(RootedTree.Forest.alpha F)

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

δσ = σ F' − σ F (MCB §3.5.2.1): yield; = 1 is "minimality of yield".

Equations

• Minimalist.Merge.δσ F F' = ↑(RootedTree.Forest.sigma F') - ↑(RootedTree.Forest.sigma F)

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

The grading consistency relation δσ = δα − δb₀, from σ = b₀ + α.

Minimal Yield as the grading conditions (MCB §3.5.2.1)

theorem Minimalist.Merge.minimalYieldWeak_iff {α : Type u_1} {β : Type u_2} (F F' : RootedTree.Forest (RootedTree.Nonplanar (α ⊕ β))) : MinimalYieldWeak F F' ↔ 0 ≤ δb₀ F F' ∧ 0 ≤ δα F F'

Weak Minimal Yield is exactly δb₀ ≥ 0 ∧ δα ≥ 0 (MCB §3.5.2.1, "no divergence / no information loss").

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

Minimal Yield is exactly δb₀ ≥ 0 ∧ δα ≥ 0 ∧ δσ = 1 (MCB §3.5.2.1).

The grading monomial and the polar part (bridge to MCB Prop. 3.5.2)

noncomputable def Minimalist.Merge.gradeMonomial {A : Type u_3} [CommRing A] (d : ℤ) : LaurentSeries A

The Laurent grading monomial tᵈ (MCB eq. 3.5.6, coefficient 1): a derivation graded by d contributes tᵈ to the Laurent-series character.

Equations

• Minimalist.Merge.gradeMonomial d = (HahnSeries.single d) 1

theorem Minimalist.Merge.polarHahn_gradeMonomial {A : Type u_3} [CommRing A] (d : ℤ) : (gradeMonomial d).polarHahn = if d < 0 then gradeMonomial d else 0

A graded monomial is polar (fixed by R = polarHahn) iff its grading is negative, and is annihilated by R otherwise — the divergent/convergent split of MCB Prop. 3.5.2.

Per-merge polarity: Minimal Yield is nonpolar, divergent Sideward is polar

theorem Minimalist.Merge.polarHahn_gradeMonomial_of_minimalYieldWeak {α : Type u_1} {β : Type u_2} {A : Type u_3} [CommRing A] (F F' : RootedTree.Forest (RootedTree.Nonplanar (α ⊕ β))) (h : MinimalYieldWeak F F') : (gradeMonomial (δb₀ F F')).polarHahn = 0

A weak-Minimal-Yield step is nonpolar in the δb₀ grading: R annihilates its monomial (δb₀ ≥ 0). The External/Internal-Merge shadow of MCB Lemma 3.5.5.

theorem Minimalist.Merge.polarHahn_gradeMonomial_em {α : Type u_1} {β : Type u_2} {A : Type u_3} [CommRing A] (lbl : α) (S S' : RootedTree.Nonplanar (α ⊕ β)) : (gradeMonomial (δb₀ {S, S'} {RootedTree.Nonplanar.node (Sum.inl lbl) {S, S'}})).polarHahn = 0

External Merge is nonpolar (MCB Lemma 3.5.5): δb₀ = +1 ≥ 0, so R annihilates its monomial.

theorem Minimalist.Merge.δb₀_sideward_3a {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : RootedTree.Nonplanar (α ⊕ β)) : δb₀ {T_i} {Tnode, T_iq} = -1

Sideward Merge 3(a) has divergent grading δb₀ = −1 (b₀ increases by one).

theorem Minimalist.Merge.δb₀_sideward_3b {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : RootedTree.Nonplanar (α ⊕ β)) : δb₀ {T_i, T_j} {Tnode, T_iq, T_jq} = -1

Sideward Merge 3(b) has divergent grading δb₀ = −1 (b₀ increases by one).

theorem Minimalist.Merge.polarHahn_gradeMonomial_sideward_3a {α : Type u_1} {β : Type u_2} {A : Type u_3} [CommRing A] (T_i Tnode T_iq : RootedTree.Nonplanar (α ⊕ β)) : (gradeMonomial (δb₀ {T_i} {Tnode, T_iq})).polarHahn = gradeMonomial (δb₀ {T_i} {Tnode, T_iq})

Sideward Merge 3(a) is polar in the δb₀ grading: R fixes its monomial (δb₀ = −1 < 0) — the divergent derivation MCB Prop. 3.5.6's Birkhoff factorization eliminates.

theorem Minimalist.Merge.polarHahn_gradeMonomial_sideward_3b {α : Type u_1} {β : Type u_2} {A : Type u_3} [CommRing A] (T_i T_j Tnode T_iq T_jq : RootedTree.Nonplanar (α ⊕ β)) : (gradeMonomial (δb₀ {T_i, T_j} {Tnode, T_iq, T_jq})).polarHahn = gradeMonomial (δb₀ {T_i, T_j} {Tnode, T_iq, T_jq})

Sideward Merge 3(b) is polar in the δb₀ grading (δb₀ = −1 < 0).