Vertex conservation for the Δ^ρ / Δᵈ (deletion) cut enumeration

[MCB25]

The deletion coproduct cutSummandsP (MCB Δ^ρ, Def. 1.2.6) extracts a crown forest and leaves the remainder ρ_C(T) — the cut subtrees are removed entirely (no trace placeholder), so vertices are conserved exactly: Σ #V(crown) + #V(trunk) = #V(T) (cutSummandsP_numNodes), with no +#cuts correction (contrast the trace variant, which adds one replacement leaf per cut).

MCB's Δᵈ (Def. 1.2.5) rebinarizes the remainder via contractUnary; each contracted unary node drops one vertex, giving the +2-per-cut accessible-term extraction (eq. 1.6.7) downstream.

theorem RootedTree.ConnesKreimer.cutSummandsP_numNodes {α : Type u_1} (t : RoseTree α) (p : Forest (RoseTree α) × RoseTree α) : p ∈ cutSummandsP t → (Multiset.map RoseTree.numNodes p.1).sum + p.2.numNodes = t.numNodes

Vertex conservation for the deletion cut enumeration (tree level): crown vertices plus trunk vertices recover the tree's vertices exactly.

theorem RootedTree.ConnesKreimer.cutListSummandsP_numNodes {α : Type u_1} (cs : List (RoseTree α)) (q : Forest (RoseTree α) × List (RoseTree α)) : q ∈ cutListSummandsP cs → (Multiset.map RoseTree.numNodes q.1).sum + (List.map RoseTree.numNodes q.2).sum = (List.map RoseTree.numNodes cs).sum

Mutual aux: vertex conservation for children-list deletion cut summands.

theorem RootedTree.ConnesKreimer.augActionP_numNodes {α : Type u_1} (t : RoseTree α) (a : Forest (RoseTree α) × Option (RoseTree α)) : a ∈ augActionP t → (Multiset.map RoseTree.numNodes a.1).sum + RootedTree.ConnesKreimer.optNumNodes✝ a.2 = t.numNodes

Mutual aux: vertex conservation for per-child deletion actions.

Nonplanar descent + Δᵈ extraction

theorem RootedTree.ConnesKreimer.cutSummandsN_numNodes {α : Type u_1} (T : Nonplanar α) (p : Forest (Nonplanar α) × Nonplanar α) : p ∈ cutSummandsN T → (Multiset.map Nonplanar.numNodes p.1).sum + p.2.numNodes = T.numNodes

Vertex conservation for the nonplanar deletion cuts, descended from cutSummandsP_numNodes.

theorem RootedTree.ConnesKreimer.cutSummandsN_crown_ne_singleton {α : Type u_1} (T : Nonplanar α) (p : Forest (Nonplanar α) × Nonplanar α) (hp : p ∈ cutSummandsN T) : p.1 ≠ {T}

No proper cut extracts the whole tree as its crown. For any cut summand p ∈ cutSummandsN T, the crown forest p.1 is never the singleton {T}. The full-tree extraction is the separate ofTree T ⊗ 1 term of comulTreeN, not a member of cutSummandsN T. Derived from vertex conservation (cutSummandsN_numNodes) plus numNodes_pos: a {T} crown would force the trunk to have zero vertices. Load-bearing for the Merge cross-term elimination (Minimalist.Merge.mergeOp_pair).

theorem RootedTree.ConnesKreimer.cutSummandsN_self_not_mem_crown {α : Type u_1} (T : Nonplanar α) (p : Forest (Nonplanar α) × Nonplanar α) (hp : p ∈ cutSummandsN T) : T ∉ p.1

No cut of T has T itself in its crown. Every crown component is a proper part of T, so it has strictly fewer vertices than T; the full-size T cannot be a crown member. From vertex conservation (cutSummandsN_numNodes) plus numNodes_pos. Mirrors legacy CutShape.not_mem_cutForest_self; load-bearing for the Sideward cross-term elimination (Minimalist.Merge.mergeOp_sideward_2b/3b).

theorem RootedTree.ConnesKreimer.cutSummandsN_accCount_single_deletion {α : Type u_1} (T : Nonplanar α) (p : Forest (Nonplanar α) × Nonplanar α) (hp : p ∈ cutSummandsN T) (mover : Nonplanar α) (hcard : p.1 = {mover}) (huc : p.2.unaryCount = 1) : T.accCount = mover.accCount + p.2.contractUnary.accCount + 2

Single-cut Δᵈ accessible-term extraction (MCB eq. 1.6.7): deleting one accessible subtree mover from T and rebinarizing the remainder (contractUnary p.2) removes two accessible terms — the subtree's edge and the contracted parent. The hypothesis unaryCount p.2 = 1 characterizes a single edge cut at a binary node (exactly one unary node is created).