Admissible-cut enumeration on rose trees

[MCB25] [Foi]

The combinatorics of admissible cuts, independent of the Hopf-algebra structures built on it in Core/Algebra/RootedTree/Coproduct/: the policy-parameterized enumeration (cutSummandsG), its Δ^ρ instance (cutSummandsP) and Δ^c instance (extractC, cutSummandsCP), the projections to RoseTree.Nonplanar with their Perm-invariance (cutSummandsN, cutSummandsCN), and the single-cut count (countSingleCutsRho).

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. 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 ConnesKreimer.cutSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Multiset (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 ConnesKreimer.cutListSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : List (RoseTree α) → Multiset (Multiset (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.
• ConnesKreimer.cutListSummandsG extract [] = {(0, [])}

@[irreducible]

def ConnesKreimer.augActionG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Multiset (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 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 : Multiset (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (cutListSummandsG extract cs)

Recursive formula on a node: cutSummandsG unfolds via cutListSummandsG.

@[simp]

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

Recursive formula for cutListSummandsG on empty list.

@[simp]

theorem ConnesKreimer.cutListSummandsG_cons {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsG extract (t :: ts) = Multiset.map (fun (p : (Multiset (RoseTree α) × List (RoseTree α)) × Multiset (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 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 : Multiset (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Recursive formula for augActionG.

theorem 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 : Multiset (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 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 : Multiset (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 (Trace.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 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 : Multiset (RoseTree α) × RoseTree α) : p ∈ cutSummandsG extract t → (Multiset.map RoseTree.numNodes p.1).sum + p.2.numNodes = t.numNodes + p.1.card

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 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 : Multiset (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 + q.1.card

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

theorem 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 : Multiset (RoseTree α) × List (RoseTree α)) : a ∈ augActionG extract t → (Multiset.map RoseTree.numNodes a.1).sum + (List.map RoseTree.numNodes a.2).sum = t.numNodes + a.1.card

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

Sanity: cuts of a leaf are just the empty cut

cutSummandsP — multiset of (cut forest, deletion remainder) pairs

Recursive enumeration of cut summands. For a leaf, the only cut is the empty cut. For a node, sum over all per-child decisions: each child can either be extracted whole (contributes to cut forest, drops from remainder) OR recurse with a smaller cut (contributes whatever its cut extracts, leaves its deletion-remainder in the remainder list).

This bespoke block is the deletion (Δ^ρ) sibling of the extraction-policy-parameterized cutSummandsG. It is deliberately NOT re-expressed as cutSummandsG (fun _ => some []): the Δ^ρ consumers are written against the Option remainder encoding used here — deletion is Option.none, a surviving child is Option.some r — whereas cutSummandsG carries List remainders (deletion [], survival [r]). Folding onto cutSummandsG would change the public return type of augActionP and the shapes of augActionP_eq/cutListSummandsP_cons, so the two enumerations coexist. (Δ^c does derive from cutSummandsG, being written against the List encoding.)

@[irreducible]

def ConnesKreimer.cutSummandsP {α : Type u_1} : RoseTree α → Multiset (Multiset (RoseTree α) × RoseTree α)

Multiset of (cut forest, deletion remainder) pairs for a tree. Each summand corresponds to one admissible cut on T under the deletion semantics.

Equations

• ConnesKreimer.cutSummandsP (RoseTree.node a cs) = Multiset.map (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (ConnesKreimer.cutListSummandsP cs)

@[irreducible]

def ConnesKreimer.cutListSummandsP {α : Type u_1} : List (RoseTree α) → Multiset (Multiset (RoseTree α) × List (RoseTree α))

Auxiliary: cut summands for a list of children. The remainder is a list (children of the parent that survived the cut).

Equations

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

@[irreducible]

def ConnesKreimer.augActionP {α : Type u_1} : RoseTree α → Multiset (Multiset (RoseTree α) × Option (RoseTree α))

Auxiliary: per-child action — either extract whole (none remainder) or recurse with a cut (some remainder).

Equations

• ConnesKreimer.augActionP x✝ = ({x✝}, none) ::ₘ Multiset.map (fun (p : Multiset (RoseTree α) × RoseTree α) => (p.1, some p.2)) (ConnesKreimer.cutSummandsP x✝)

@[simp]

theorem ConnesKreimer.cutSummandsP_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : cutSummandsP (RoseTree.node a cs) = Multiset.map (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (cutListSummandsP cs)

Recursive formula on a node: cutSummandsP unfolds via cutListSummandsP.

@[simp]

theorem ConnesKreimer.cutListSummandsP_nil {α : Type u_1} : cutListSummandsP [] = {(0, [])}

Recursive formula for cutListSummandsP on empty list.

@[simp]

theorem ConnesKreimer.cutListSummandsP_cons {α : Type u_1} (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsP (t :: ts) = Multiset.map (fun (p : (Multiset (RoseTree α) × Option (RoseTree α)) × Multiset (RoseTree α) × List (RoseTree α)) => match p.1.2 with | none => (p.1.1 + p.2.1, p.2.2) | some r => (p.1.1 + p.2.1, r :: p.2.2)) (augActionP t ×ˢ cutListSummandsP ts)

Recursive formula for cutListSummandsP on a cons list.

@[simp]

theorem ConnesKreimer.augActionP_eq {α : Type u_1} (t : RoseTree α) : augActionP t = ({t}, none) ::ₘ Multiset.map (fun (p : Multiset (RoseTree α) × RoseTree α) => (p.1, some p.2)) (cutSummandsP t)

Recursive formula for augActionP.

def ConnesKreimer.combineP_fn {α : Type u_1} : (Multiset (RoseTree α) × Option (RoseTree α)) × Multiset (RoseTree α) × List (RoseTree α) → Multiset (RoseTree α) × List (RoseTree α)

Named version of the combine_P function (extracted to avoid Lean's "inline match generates fresh matchers" issue when this is reused across proofs via rewrite).

Equations

• ConnesKreimer.combineP_fn p = match p.1.2 with | none => (p.1.1 + p.2.1, p.2.2) | some r => (p.1.1 + p.2.1, r :: p.2.2)

theorem ConnesKreimer.cutListSummandsP_cons' {α : Type u_1} (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsP (t :: ts) = Multiset.map combineP_fn (augActionP t ×ˢ cutListSummandsP ts)

Projection of cut summands and descent to Nonplanar

To descend Δ^ρ from RoseTree to Nonplanar, we need a Nonplanar-side cut-summand multiset that is Perm-invariant. The strategy: project each tree-level cut summand through mk componentwise, then prove the resulting multiset depends on T : RoseTree α only through mk T.

The proof factors through three layers:

• Pointwise projection (projSummand, projForest, projAugAction): the per-element Nonplanar.mk lifts.
• Combine factoring (cutListSummandsP_cons_proj): the cons case of cutListSummandsP distributes over the projection, giving a clean cartesian-product recursion at the Nonplanar level.
• Headline recursion (cutSummandsP_proj_perm with its PermList companion cutListSummandsP_proj_permList, and the derived cutListSummandsP_proj_componentwise): structural recursion over the mutual Perm/PermList for the substantive content; a pure List.Forall₂ lift for the rest.

Pointwise projection

def ConnesKreimer.projSummand {α : Type u_1} : Multiset (RoseTree α) × RoseTree α → Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α

Project a tree-level cut summand to a nonplanar one.

Equations

• ConnesKreimer.projSummand p = (Multiset.map RoseTree.Nonplanar.mk p.1, RoseTree.Nonplanar.mk p.2)

def ConnesKreimer.projForest {α : Type u_1} : Multiset (RoseTree α) × List (RoseTree α) → Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)

Project a cutListSummandsP summand to nonplanar level, discarding the list-order of the remainder children. The discarded order doesn't affect the eventual mk (.node a remainder), since mk is invariant under children-list permutation (RoseTree.Perm.node_of_perm).

Equations

• ConnesKreimer.projForest p = (Multiset.map RoseTree.Nonplanar.mk p.1, ↑(List.map RoseTree.Nonplanar.mk p.2))

def ConnesKreimer.projAugAction {α : Type u_1} : Multiset (RoseTree α) × Option (RoseTree α) → Multiset (RoseTree.Nonplanar α) × Option (RoseTree.Nonplanar α)

Project an augActionP summand to nonplanar level (per-child decision).

Equations

• ConnesKreimer.projAugAction p = (Multiset.map RoseTree.Nonplanar.mk p.1, Option.map RoseTree.Nonplanar.mk p.2)

theorem ConnesKreimer.projSummand_node_factors {α : Type u_1} (a : α) (p : Multiset (RoseTree α) × List (RoseTree α)) : projSummand (p.1, RoseTree.node a p.2) = ((projForest p).1, RoseTree.Nonplanar.node a (projForest p).2)

Bridge: applying cutSummandsP_node's wrapper (p.1, .node a p.2) then projSummand factors through projForest followed by the Nonplanar.node a smart constructor.

Combine factoring through projection

The cons case of cutListSummandsP combines a per-child decision (augActionP) with the cut-summands of the remaining children. This combination distributes over the Nonplanar projection: the "projected combiner" innerCombinerProj operates on (Forest × Option) × (Forest × Multiset) and matches projForest of the inline tree-level combiner. The headline result is cutListSummandsP_cons_proj, which expresses the cons case of the projected cutListSummandsP as a clean cartesian product at the Nonplanar level.

def ConnesKreimer.innerCombinerProj {α : Type u_1} : (Multiset (RoseTree.Nonplanar α) × Option (RoseTree.Nonplanar α)) × Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α) → Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)

The Nonplanar-level combiner: given a per-child decision and the accumulated cuts of the remaining children, produce the merged (cut forest, remainder multiset) pair. Mirrors the inline lambda in cutListSummandsP's cons case but operates on Multiset remainders.

Equations

• ConnesKreimer.innerCombinerProj ((F, none), G, ms) = (F + G, ms)
• ConnesKreimer.innerCombinerProj ((F, some r), G, ms) = (F + G, r ::ₘ ms)

Cartesian-product distributivity

The pair-componentwise Prod.map distributes over Multiset.product (×ˢ). Mathlib has the bind-side analogues but not this exact form for multiset products; the proof is one inductive line via cons_product.

Headline factoring: cons case of projected cutListSummandsP

theorem ConnesKreimer.cutListSummandsP_cons_proj {α : Type u_1} (t : RoseTree α) (ts : List (RoseTree α)) : Multiset.map projForest (cutListSummandsP (t :: ts)) = Multiset.map innerCombinerProj (Multiset.map projAugAction (augActionP t) ×ˢ Multiset.map projForest (cutListSummandsP ts))

The projected cutListSummandsP on a cons list factors as a clean cartesian product at the Nonplanar level. This is the key lemma enabling all subsequent invariance proofs.

List-side projection invariants

These three theorems establish that the projected cutListSummandsP is invariant under (1) substituting an "augAction-projection-equal" child, (2) substituting a "projForest-equal" tail, and (3) any list permutation.

theorem ConnesKreimer.innerCombinerProj_swap_args {α : Type u_1} (a b : Multiset (RoseTree.Nonplanar α) × Option (RoseTree.Nonplanar α)) (c : Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) : innerCombinerProj (a, innerCombinerProj (b, c)) = innerCombinerProj (b, innerCombinerProj (a, c))

Triple-combiner symmetry: combining three pieces (two decisions plus the accumulated rest) at the projected level is symmetric in the first two decision arguments.

theorem ConnesKreimer.swap_double_combinerProj {α : Type u_1} (A B : Multiset (Multiset (RoseTree.Nonplanar α) × Option (RoseTree.Nonplanar α))) (C : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))) : Multiset.map innerCombinerProj (A ×ˢ Multiset.map innerCombinerProj (B ×ˢ C)) = Multiset.map innerCombinerProj (B ×ˢ Multiset.map innerCombinerProj (A ×ˢ C))

Doubly-applied innerCombinerProj over a triple cartesian product is symmetric in the first two factors. The substantive content of cutListSummandsP_proj_perm's swap case.

theorem ConnesKreimer.cutListSummandsP_proj_perm {α : Type u_1} {cs ds : List (RoseTree α)} (h : cs.Perm ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

The projected cutListSummandsP is List.Perm-invariant: two permutation-related child lists yield the same projected cut-summand multiset.

Headline: Perm + PermList recursion

Structural recursion over the mutual Perm/PermList. The node case lifts the companion's list-level equality through the Nonplanar.node a wrapper; the PermList.cons case changes the head child then the tail; the PermList.swap case reorders identical siblings (cutListSummandsP_proj_perm).

theorem ConnesKreimer.cutSummandsP_proj_perm {α : Type u_1} {t s : RoseTree α} : t.Perm s → Multiset.map projSummand (cutSummandsP t) = Multiset.map projSummand (cutSummandsP s)

Projection invariance of cutSummandsP under Perm.

theorem ConnesKreimer.cutListSummandsP_proj_componentwise {α : Type u_1} {cs ds : List (RoseTree α)} (h : List.Forall₂ RoseTree.Perm cs ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

Componentwise Perm invariance for child lists, from the PermList companion via PermList.of_forall₂.

Δ^ρ on Nonplanar via descent

The cutSummandsP_proj_perm invariance lifts cutSummandsP through Nonplanar.lift, giving a well-defined cutSummandsN. The tree-level coproduct comulTreeN then extends multiplicatively to a forest-level monoid hom and finally to the algebra hom comulAlgHomN.

noncomputable def ConnesKreimer.cutSummandsN {α : Type u_1} : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)

The Nonplanar cut-summand multiset, defined via Nonplanar.lift using the cutSummandsP_proj_perm invariance.

Equations

• ConnesKreimer.cutSummandsN = RoseTree.Nonplanar.lift (fun (T : RoseTree α) => Multiset.map ConnesKreimer.projSummand (ConnesKreimer.cutSummandsP T)) ⋯

@[simp]

theorem ConnesKreimer.cutSummandsN_mk {α : Type u_1} (T : RoseTree α) : cutSummandsN (RoseTree.Nonplanar.mk T) = Multiset.map projSummand (cutSummandsP T)

theorem ConnesKreimer.cutSummandsN_leaf {α : Type u_1} (a : α) : cutSummandsN (RoseTree.Nonplanar.leaf a) = {(0, RoseTree.Nonplanar.leaf a)}

The cut summands of a leaf: only the empty cut (0, leaf a).

noncomputable def ConnesKreimer.countSingleCutsRho {α : Type u_1} [DecidableEq α] (T T₁ T₂ : RoseTree.Nonplanar α) : ℕ

Number of Δ^ρ cut summands of T whose cut forest is {T₁} and whose remainder tree is T₂ — the Δ^ρ analog of the count c^T_{T₁,T₂} of [MCB25].

Equations

• ConnesKreimer.countSingleCutsRho T T₁ T₂ = Multiset.countP (fun (p : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α) => p.1 = {T₁} ∧ p.2 = T₂) (ConnesKreimer.cutSummandsN T)

augActionN and cutForestSummandsN substrate

cutForestSummandsN F is the Nonplanar-level multiset of (cut_forest, remainder_forest) pairs ranging over per-tree decisions on the forest F. Each per-tree decision (augActionN T) is either "extract T whole" (pair ({T}, none)) or "recurse with a cut summand of T" (pair (s.1, some s.2) for s ∈ cutSummandsN T).

Defined recursively at the Nonplanar level via Multiset.foldr, with the LeftCommutative obligation discharged by swap_double_combinerProj (the per-tree-decision swap symmetry, established for the tree-level projection in §3 above and reused here verbatim).

noncomputable def ConnesKreimer.augActionN {α : Type u_1} (T : RoseTree.Nonplanar α) : Multiset (Multiset (RoseTree.Nonplanar α) × Option (RoseTree.Nonplanar α))

Per-tree decision multiset at the Nonplanar level: extract this tree whole (({T}, none)), or recurse into a cut summand.

Equations

• ConnesKreimer.augActionN T = ({T}, none) ::ₘ Multiset.map (fun (s : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α) => (s.1, some s.2)) (ConnesKreimer.cutSummandsN T)

theorem ConnesKreimer.augActionN_mk {α : Type u_1} (T : RoseTree α) : augActionN (RoseTree.Nonplanar.mk T) = Multiset.map projAugAction (augActionP T)

Bridge to the tree-level augActionP: at a tree-level lift, augActionN agrees with (augActionP T).map projAugAction.

noncomputable def ConnesKreimer.cutForestSummandsN {α : Type u_1} (F : Multiset (RoseTree.Nonplanar α)) : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))

The forest cut summand multiset: every per-tree decision tuple on F : Multiset (Nonplanar α) produces a pair (cut_forest, remainder_forest), and cutForestSummandsN F enumerates them all (as a multiset). The public Nonplanar-level analog of (cutListSummandsP ps).map projForest, independent of the tree-level list representation.

Equations

• ConnesKreimer.cutForestSummandsN F = Multiset.foldr ConnesKreimer.cutForestCombinerN✝ {(0, 0)} F

@[simp]

theorem ConnesKreimer.cutForestSummandsN_zero {α : Type u_1} : cutForestSummandsN 0 = {(0, 0)}

@[simp]

theorem ConnesKreimer.cutForestSummandsN_cons {α : Type u_1} (T : RoseTree.Nonplanar α) (F : Multiset (RoseTree.Nonplanar α)) : cutForestSummandsN (T ::ₘ F) = Multiset.map innerCombinerProj (augActionN T ×ˢ cutForestSummandsN F)

Bridges to the tree-level list representation

The tree-level substrate cutListSummandsP (defined on List (RoseTree α)) evaluates cutForestSummandsN on a tree-level list rep and characterizes cuts of a Nonplanar node (cutSummandsN_node).

theorem ConnesKreimer.cutForestSummandsN_via_planar_list {α : Type u_1} (ps : List (RoseTree α)) : cutForestSummandsN ↑(List.map RoseTree.Nonplanar.mk ps) = Multiset.map projForest (cutListSummandsP ps)

cutForestSummandsN evaluated on a tree-level list rep agrees with the tree-level cutListSummandsP projected through projForest. By induction on ps using cutListSummandsP_cons_proj and augActionN_mk.

theorem ConnesKreimer.cutSummandsN_node_planar_list {α : Type u_1} (a : α) (ps : List (RoseTree α)) : cutSummandsN (RoseTree.Nonplanar.node a ↑(List.map RoseTree.Nonplanar.mk ps)) = Multiset.map (fun (pf : Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) => (pf.1, RoseTree.Nonplanar.node a pf.2)) (Multiset.map projForest (cutListSummandsP ps))

Cuts of a node decompose via the tree-level cutListSummandsP projected through projForest — the tree-level-list-rep form of cutSummandsN_node. The map (p ↦ (p.1, Nonplanar.node a p.2)) re-grafts the remainder children onto a fresh root with label a.

@[simp]

theorem ConnesKreimer.cutSummandsN_node {α : Type u_1} (a : α) (F : Multiset (RoseTree.Nonplanar α)) : cutSummandsN (RoseTree.Nonplanar.node a F) = Multiset.map (fun (pf : Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) => (pf.1, RoseTree.Nonplanar.node a pf.2)) (cutForestSummandsN F)

Cuts of Nonplanar.node a F decompose along the per-tree decisions of F: each pair (cf, rem) ∈ cutForestSummandsN F gives a cut summand (cf, Nonplanar.node a rem). The Nonplanar-level form.

traceLeaf — placeholder for a cut subtree

def ConnesKreimer.traceLeaf {α : Type u_1} {β : Type u_2} (b : β) : RoseTree (α ⊕ β)

The trace-marker placeholder leaf carrying the encoded label b : β.

Equations

• ConnesKreimer.traceLeaf b = RoseTree.node (Sum.inr b) []

Δ^c extraction policy

def ConnesKreimer.extractC {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))

The Δ^c extraction policy: for Sum.inl-rooted (non-trace) subtrees, extract whole leaving a single traceLeaf (τ t) in the parent's child slot. For Sum.inr-rooted (trace) subtrees, decline to extract.

Declining at trace subtrees is required for coassociativity — without it, iterated Δ^c produces "trace of trace" right-channel terms that break the double-cut bijection — and matches [MCB25] Definition 1.2.2's restriction of cuts to accessible terms, which excludes trace placeholders.

Equations

• ConnesKreimer.extractC τ (RoseTree.node (Sum.inl val) children) = some [ConnesKreimer.traceLeaf (τ (RoseTree.node (Sum.inl val) children))]
• ConnesKreimer.extractC τ (RoseTree.node (Sum.inr val) children) = none

@[simp]

theorem ConnesKreimer.extractC_inl {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α) (cs : List (RoseTree (α ⊕ β))) : extractC τ (RoseTree.node (Sum.inl a) cs) = some [traceLeaf (τ (RoseTree.node (Sum.inl a) cs))]

@[simp]

theorem ConnesKreimer.extractC_inr {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (b : β) (cs : List (RoseTree (α ⊕ β))) : extractC τ (RoseTree.node (Sum.inr b) cs) = none

cutSummandsCP — Δ^c cut enumeration via the generic cutSummandsG

Defined as cutSummandsG (extractC τ). The generic-side simp lemmas (cutSummandsG_node, cutListSummandsG_*, augActionG_*) compose with extractC_inl/extractC_inr to give the Δ^c-specific reductions.

def ConnesKreimer.cutSummandsCP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : RoseTree (α ⊕ β) → Multiset (Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β))

The Δ^c cut summands: cuts at non-trace subtrees with trace placeholders, skipping cuts at trace leaves.

Equations

• ConnesKreimer.cutSummandsCP τ = ConnesKreimer.cutSummandsG (ConnesKreimer.extractC τ)

theorem ConnesKreimer.cutSummandsCP_def {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (T : RoseTree (α ⊕ β)) : cutSummandsCP τ T = cutSummandsG (extractC τ) T

@[simp]

theorem ConnesKreimer.cutSummandsCP_node {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : cutSummandsCP τ (RoseTree.node a cs) = Multiset.map (fun (p : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) => (p.1, RoseTree.node a p.2)) (cutListSummandsG (extractC τ) cs)

Sanity: the trace policy on leaves

Descent of cut-summand enumeration

Mirrors Coproduct/Pruning.lean's descent of cutSummandsP, but for the generic cutSummandsG (which uses a List-shaped per-cut remainder rather than Option). The descent applies whenever the extract policy is invariant under RoseTree.Perm modulo Nonplanar.mk. For Δ^c (extractC (τ ∘ Nonplanar.mk)) this follows from Perm.value_eq.

Pointwise projection for the G-form

Bridge: projSummand factors through projForestG + node

Combiner factoring

The cons case of cutListSummandsG adds the cut forest and concatenates the remainder lists. At the Nonplanar level (via projForestG), the remainder concatenation becomes multiset addition.

def ConnesKreimer.combinerProjG {α : Type u_1} : (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) × Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α) → Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)

The Nonplanar-level combiner: clean addition on both components.

Equations

• ConnesKreimer.combinerProjG ((F1, m1), F2, m2) = (F1 + F2, m1 + m2)

Cartesian-product distributivity (G-form copy)

theorem ConnesKreimer.map_prodMap_product_G {α' : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_6} (f : α' → γ) (g : β' → δ) (s : Multiset α') (t : Multiset β') : Multiset.map (Prod.map f g) (s ×ˢ t) = Multiset.map f s ×ˢ Multiset.map g t

Headline factoring: cons case of projected cutListSummandsG

Extract-policy invariance

The hypothesis on the extract policy: its return value, projected component-wise through Nonplanar.mk, is the same on Perm-equal inputs. For Δ^c (extractC (τ ∘ Nonplanar.mk)) this holds because the root label and the τ value are both Perm-invariant.

def ConnesKreimer.ExtractInvariant {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : Prop

An extract policy is Nonplanar.mk-invariant if its return value, projected componentwise through Nonplanar.mk, depends on its input only through Nonplanar.mk.

Equations

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

List-side projection invariants

Three theorems parallel to cutListSummandsP_proj_at_via_augAction, cutListSummandsP_proj_tail_lift, and cutListSummandsP_proj_perm.

Swap symmetry for combinerProjG

theorem ConnesKreimer.combinerProjG_swap_args {α : Type u_1} (a b c : Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) : combinerProjG (a, combinerProjG (b, c)) = combinerProjG (b, combinerProjG (a, c))

Triple-combiner symmetry: combining three projected pieces at the Nonplanar level is symmetric in the first two factors.

theorem ConnesKreimer.swap_double_combinerProjG {α : Type u_1} (A B C : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))) : Multiset.map combinerProjG (A ×ˢ Multiset.map combinerProjG (B ×ˢ C)) = Multiset.map combinerProjG (B ×ˢ Multiset.map combinerProjG (A ×ˢ C))

Doubly-applied combinerProjG over a triple cartesian product is symmetric in the first two factors. The substantive content of cutListSummandsG_proj_perm's swap case.

Headline: Perm + PermList recursion

Structural recursion over the mutual Perm/PermList. The node case lifts the companion's list-level equality through the Nonplanar.node a wrapper; the PermList.cons case changes the head child (via cutSummandsG_proj_perm and augActionG_proj_eq_of_step_data) then the tail; the PermList.swap case is the identical-siblings reorder (cutListSummandsG_proj_perm).

theorem ConnesKreimer.cutSummandsG_proj_perm {α : Type u_1} {extract : RoseTree α → Option (List (RoseTree α))} (hExt : ExtractInvariant extract) {t s : RoseTree α} : t.Perm s → Multiset.map projSummand (cutSummandsG extract t) = Multiset.map projSummand (cutSummandsG extract s)

Projection invariance of cutSummandsG under Perm.

Generic cut convolution: treeCutsG and forestCutsG

All cut summands of a tree as (crown forest, trunk forest) pairs — the full cut ({T}, 0) plus each cuts-summand with a singleton trunk — and their combinerProjG-convolution over the trees of a forest. The generic coproduct expands as a single sum over these (comulTreeNG_eq_sum/comulForestNG_eq_sum, Coproduct/WithCuts.lean).

noncomputable def ConnesKreimer.treeCutsG {α : Type u_1} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (T : RoseTree.Nonplanar α) : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))

All cut summands of a tree as (crown, trunk-forest) pairs: the full cut ({T}, 0) plus each summand of cuts T with a singleton trunk.

Equations

• ConnesKreimer.treeCutsG cuts T = ({T}, 0) ::ₘ Multiset.map (fun (p : Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α) => (p.1, {p.2})) (cuts T)

instance ConnesKreimer.instLeftCommConvCut {α : Type u_1} : LeftCommutative fun (s acc : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))) => Multiset.map combinerProjG (s ×ˢ acc)

Convolution-of-cuts is left-commutative (it is the symmetric combinerProjG); needed for Multiset.foldr.

noncomputable def ConnesKreimer.forestCutsG {α : Type u_1} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (F : Multiset (RoseTree.Nonplanar α)) : Multiset (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α))

Forest-level cut enumeration: combinerProjG-convolution of treeCutsG over the component trees.

Equations

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

theorem ConnesKreimer.forestCutsG_zero {α : Type u_1} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : forestCutsG cuts 0 = {(0, 0)}

theorem ConnesKreimer.forestCutsG_cons {α : Type u_1} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (T : RoseTree.Nonplanar α) (F : Multiset (RoseTree.Nonplanar α)) : forestCutsG cuts (T ::ₘ F) = Multiset.map combinerProjG (treeCutsG cuts T ×ˢ forestCutsG cuts F)

theorem ConnesKreimer.cutForestSummandsN_eq_forestCutsG {α : Type u_1} (F : Multiset (RoseTree.Nonplanar α)) : cutForestSummandsN F = forestCutsG cutSummandsN F

The Δ^ρ forest cut enumeration is the generic convolution at cuts := cutSummandsN: augActionN (Option-encoded) and treeCutsG cutSummandsN (forest-encoded) enumerate the same per-tree decisions, and innerCombinerProj matches combinerProjG across the encoding.

Trace specialization

The Δ^c policy extractC (τ ∘ Nonplanar.mk) is ExtractInvariant:

• For Sum.inl _-rooted inputs, extractC returns some [traceLeaf (τ (mk t))].
• For Sum.inr _-rooted inputs, extractC returns none.

Both cases are determined by the root label and the τ value, both of which are Perm-invariant.

theorem ConnesKreimer.extractC_mkComp_invariant {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) : ExtractInvariant (extractC (τ ∘ RoseTree.Nonplanar.mk))

The Δ^c extract policy is ExtractInvariant.

theorem ConnesKreimer.cutSummandsCP_proj_perm {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) {t s : RoseTree (α ⊕ β)} (h : t.Perm s) : Multiset.map projSummand (cutSummandsCP (τ ∘ RoseTree.Nonplanar.mk) t) = Multiset.map projSummand (cutSummandsCP (τ ∘ RoseTree.Nonplanar.mk) s)

Δ^c cut-summand-projection invariance under Perm.

Descent of cutSummandsCP through Nonplanar.mk

noncomputable def ConnesKreimer.cutSummandsCN {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) : RoseTree.Nonplanar (α ⊕ β) → Multiset (Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β))

The Nonplanar Δ^c cut summands, descended from cutSummandsCP via Nonplanar.lift using the descent invariance cutSummandsCP_proj_perm.

Equations

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

@[simp]

theorem ConnesKreimer.cutSummandsCN_mk {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree (α ⊕ β)) : cutSummandsCN τ (RoseTree.Nonplanar.mk T) = Multiset.map projSummand (cutSummandsCP (τ ∘ RoseTree.Nonplanar.mk) T)

theorem ConnesKreimer.cutSummandsCN_edgeCount {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → RoseTree.Nonplanar.Forest.edgeCount p.1 + p.2.numNodes = T.numNodes

Edge conservation for Δ^c cut summands: the trace marker replaces the cut subtree by a unit-weight leaf, so crown edges plus trunk weight recover the tree weight exactly. Descends cutSummandsG_numNodes through Nonplanar.mk.

Empty-cut uniqueness — combinatorial substrate for the per-tree counit law

For any extract policy and tree T, the unique cut summand of cutSummandsG extract T with empty cut forest (p.1.card = 0) is the empty cut (0, T). By mutual structural induction with the list and per-child cases. This is the substrate for the Δ^c per-tree counit law: under (counit ⊗ id), only this summand survives, contributing 1 ⊗ ofTree T.

theorem ConnesKreimer.cutSummandsG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (T : RoseTree α) : Multiset.filter (fun (p : Multiset (RoseTree α) × RoseTree α) => p.1.card = 0) (cutSummandsG extract T) = {(0, T)}

The unique cut summand of cutSummandsG extract T with empty cut forest is the empty cut (0, T).

theorem ConnesKreimer.cutListSummandsG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (cs : List (RoseTree α)) : Multiset.filter (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => p.1.card = 0) (cutListSummandsG extract cs) = {(0, cs)}

The unique list-cut summand of cutListSummandsG extract cs with empty cut forest is (0, cs).

theorem ConnesKreimer.augActionG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) : Multiset.filter (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => p.1.card = 0) (augActionG extract t) = {(0, [t])}

The unique per-child decision of augActionG extract t with empty cut forest is (0, [t]) (the "recurse with empty cut" branch).

theorem ConnesKreimer.cutSummandsCN_filter_empty {α : Type u_1} {β : Type u_2} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) : Multiset.filter (fun (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) => p.1.card = 0) (cutSummandsCN τ T) = {(0, T)}

Nonplanar-level descent: the unique cut summand of cutSummandsCN τ T with empty cut forest is (0, T).