Generalized cut-summand enumeration on RoseTree α

[MCB25] [foissy-introduction-hopf-algebras-trees]

The admissible-cut enumeration parameterized by an extraction policy extract : RoseTree α → Option (List (RoseTree α)). A cut at a child position calls extract on the cut subtree:

• extract t = none — cuts at this subtree are forbidden (the "extract whole" branch is omitted).
• extract t = some [] — extract whole, leaving NOTHING in the parent's child slot (the deletion / Δ^ρ convention).
• extract t = some [r] — extract whole, leaving a single replacement leaf r in the parent's child slot (the trace / Δ^c convention).
• extract t = some [r₁, r₂, ...] — extract whole, leaving multiple replacement leaves (general; not used by current consumers).

Both Δ^ρ (deletion-style, Pruning.lean) and Δ^c (trace-preserving, Trace.lean) are specializations of this enumeration. The combinatorial cut bookkeeping is shared; only the per-cut remainder semantics varies.

Status

[UPSTREAM] candidate. Sorry-free. Substrate for the GL-duality coassoc proof of Δ^c (Foissy 2018, hal-01924416, §4.2 + Cor 4.10): once a single cut enumeration is in place, the per-cut remainder function (deletion vs trace vs other) is just a parameter to the same combinatorial bookkeeping.

MCB anchor

[MCB25] Definition 1.2.8 (book p. 33), formula (1.2.8) defines Δ^ω(T) := T ⊗ 1 + 1 ⊗ T + Σ F_v ⊗ T/^ω F_v for ω ∈ {c, d, ρ}. The three remainder semantics differ in T/^ω F_v but the cut enumeration F_v is the same. This file factors the cut enumeration out of the remainder choice.

cutSummandsG — enumeration parameterized by extract

Mirrors cutSummandsP/cutListSummandsP/augActionP (in Pruning.lean) but with the per-child decision factored through extract. The remainder type is List (RoseTree α) (zero, one, or many replacement leaves per cut), uniform across deletion and trace variants.

For Δ^ρ: extract t := some [] (always extract, leave nothing). For Δ^c: extract returns some [traceLeaf (τ t)] for Sum.inl-rooted inputs and none for Sum.inr-rooted inputs.

@[irreducible]

def RootedTree.ConnesKreimer.cutSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Forest (RoseTree α) × RoseTree α)

Multiset of (cut forest, remainder) pairs for a tree, under the extraction policy extract.

Equations

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

@[irreducible]

def RootedTree.ConnesKreimer.cutListSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : List (RoseTree α) → Multiset (Forest (RoseTree α) × List (RoseTree α))

Auxiliary: cut summands for a list of children. The remainder is a list of replacement entries — each surviving child contributes one entry (its remainder); each extracted child contributes extract t-many entries.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.ConnesKreimer.cutListSummandsG extract [] = {(0, [])}

@[irreducible]

def RootedTree.ConnesKreimer.augActionG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Forest (RoseTree α) × List (RoseTree α))

Auxiliary: per-child action under extract. The extract branch contributes ({t}, replacement) if extract t = some replacement (omitted if extract t = none). The recursive branch contributes (cut, [remainder]) for each cut summand of t.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsG_node {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (a : α) (cs : List (RoseTree α)) : cutSummandsG extract (RoseTree.node a cs) = Multiset.map (fun (p : Forest (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (cutListSummandsG extract cs)

Recursive formula on a node: cutSummandsG unfolds via cutListSummandsG.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsG_nil {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : cutListSummandsG extract [] = {(0, [])}

Recursive formula for cutListSummandsG on empty list.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsG_cons {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsG extract (t :: ts) = Multiset.map (fun (p : (Forest (RoseTree α) × List (RoseTree α)) × Forest (RoseTree α) × List (RoseTree α)) => (p.1.1 + p.2.1, p.1.2 ++ p.2.2)) (augActionG extract t ×ˢ cutListSummandsG extract ts)

Recursive formula for cutListSummandsG on a cons list.

@[simp]

theorem RootedTree.ConnesKreimer.augActionG_eq {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) : augActionG extract t = (match extract t with | none => 0 | some r => {({t}, r)}) + Multiset.map (fun (p : Forest (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Recursive formula for augActionG.

theorem RootedTree.ConnesKreimer.augActionG_eq_none {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (h : extract t = none) : augActionG extract t = Multiset.map (fun (p : Forest (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Specialized form of augActionG_eq when extract t = none: only the inherited cut summands survive.

theorem RootedTree.ConnesKreimer.augActionG_eq_some {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (r : List (RoseTree α)) (h : extract t = some r) : augActionG extract t = ({t}, r) ::ₘ Multiset.map (fun (p : Forest (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Specialized form of augActionG_eq when extract t = some r: the extract-whole branch contributes ({t}, r).

Node-count conservation under generic cuts

For extraction policies whose replacement entries carry a single node total (Δ^c's single trace leaf, extractC), every cut summand conserves vertices up to one replacement vertex per crown component: crown node count plus remainder node count equals the original node count plus the crown's component count. At the edge level this is exact conservation — the grading of MCB Lemma 1.2.10 (TraceNonplanar.lean).

A child list's total node count is (l.map RoseTree.numNodes).sum, so List.map_append/List.sum_append discharge the append step directly and RoseTree.numNodes_node unfolds the node count — no bespoke child-list recursion or append lemma is needed.

theorem RootedTree.ConnesKreimer.cutSummandsG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = 1) (t : RoseTree α) (p : Forest (RoseTree α) × RoseTree α) : p ∈ cutSummandsG extract t → (Multiset.map RoseTree.numNodes p.1).sum + p.2.numNodes = t.numNodes + Multiset.card p.1

Cut summands conserve node count (tree level): crown node count plus trunk node count equals the tree node count plus one replacement vertex per crown component. Requires single-node replacement entries.

theorem RootedTree.ConnesKreimer.cutListSummandsG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = 1) (cs : List (RoseTree α)) (q : Forest (RoseTree α) × List (RoseTree α)) : q ∈ cutListSummandsG extract cs → (Multiset.map RoseTree.numNodes q.1).sum + (List.map RoseTree.numNodes q.2).sum = (List.map RoseTree.numNodes cs).sum + Multiset.card q.1

Mutual aux: node-count conservation for children-list cut summands.

theorem RootedTree.ConnesKreimer.augActionG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = 1) (t : RoseTree α) (a : Forest (RoseTree α) × List (RoseTree α)) : a ∈ augActionG extract t → (Multiset.map RoseTree.numNodes a.1).sum + (List.map RoseTree.numNodes a.2).sum = t.numNodes + Multiset.card a.1

Mutual aux: node-count conservation for per-child actions.

Sanity: cuts of a leaf are just the empty cut