Generalized cut-summand enumeration on RootedTree.Planar α

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}

The admissible-cut enumeration parameterized by an extraction policy extract : Planar α → Option (List (Planar α)). 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, Coproduct.lean) and Δ^c (trace-preserving, CoproductDecorated.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

@cite{marcolli-chomsky-berwick-2025} 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 Coproduct.lean) but with the per-child decision factored through extract. The remainder type is List (Planar α) (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 : Planar α → Option (List (Planar α))) : Planar α → Multiset (Forest (Planar α) × Planar α)

Multiset of (cut forest, remainder) pairs for a planar 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 : Planar α → Option (List (Planar α))) : List (Planar α) → Multiset (Forest (Planar α) × List (Planar α))

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 : Planar α → Option (List (Planar α))) : Planar α → Multiset (Forest (Planar α) × List (Planar α))

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 : Planar α → Option (List (Planar α))) (a : α) (cs : List (Planar α)) : cutSummandsG extract (Planar.node a cs) = Multiset.map (fun (p : Forest (Planar α) × List (Planar α)) => (p.1, Planar.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 : Planar α → Option (List (Planar α))) : cutListSummandsG extract [] = {(0, [])}

Recursive formula for cutListSummandsG on empty list.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsG_cons {α : Type u_1} (extract : Planar α → Option (List (Planar α))) (t : Planar α) (ts : List (Planar α)) : cutListSummandsG extract (t :: ts) = Multiset.map (fun (p : (Forest (Planar α) × List (Planar α)) × Forest (Planar α) × List (Planar α)) => (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 : Planar α → Option (List (Planar α))) (t : Planar α) : augActionG extract t = (match extract t with | none => 0 | some r => {({t}, r)}) + Multiset.map (fun (p : Forest (Planar α) × Planar α) => (p.1, [p.2])) (cutSummandsG extract t)

Recursive formula for augActionG.

theorem RootedTree.ConnesKreimer.augActionG_eq_none {α : Type u_1} (extract : Planar α → Option (List (Planar α))) (t : Planar α) (h : extract t = none) : augActionG extract t = Multiset.map (fun (p : Forest (Planar α) × Planar α) => (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 : Planar α → Option (List (Planar α))) (t : Planar α) (r : List (Planar α)) (h : extract t = some r) : augActionG extract t = ({t}, r) ::ₘ Multiset.map (fun (p : Forest (Planar α) × Planar α) => (p.1, [p.2])) (cutSummandsG extract t)

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

Sanity: cuts of a leaf are just the empty cut