Measures and conservation laws for the cut enumerations

The trace-marker leaf statistics on RoseTree (α ⊕ β) and UnorderedTree (α ⊕ β) (traceLeafCount, traceDepthSum — Sum.inr marks a trace), and the size bookkeeping of the trace-preserving cut enumeration cutSummandsCN: a cut summand splits a tree into a crown forest p.1 and a trunk p.2 carrying one trace-marker leaf per cut.

Main results

• ConnesKreimer.cutSummandsCN_numNodes — weight conservation: Σ #V(crown) + #V(trunk) = #V(T) + #cuts (MCB Lemma 1.6.3).
• ConnesKreimer.cutSummandsCN_traceLeafCount — trace-leaf conservation: Σ #trace(crown) + #trace(trunk) = #trace(T) + #cuts.
• ConnesKreimer.cutSummandsCN_lexical_conservation — exact conservation of non-trace vertices.
• ConnesKreimer.cutSummandsCN_trunk_rootValue, cutSummandsCN_crown_traceLeafCount_lt_numNodes — non-degeneracy: the trunk keeps the root, crown components are lexical-rooted.
• ConnesKreimer.Cut.numContractions, ConnesKreimer.Cut.depthC — the per-cut measures (crown cardinality; trunk trace-depth sum), with Cut.depthC_pos for proper cuts of lexical-rooted trees.
• ConnesKreimer.cutSummandsP_numNodes, cutSummandsN_numNodes — exact vertex conservation for the deletion cut enumeration, with the non-degeneracy corollaries cutSummandsN_crown_ne_singleton, cutSummandsN_self_not_mem_crown and the single-deletion edge count cutSummandsN_numEdges_single_deletion.

References

• [MCB25], §1.2 and §1.6.2 (Definitions 1.2.5, 1.2.6, Lemma 1.6.3)

def RoseTree.traceLeafCount {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : ℕ

The number of Sum.inr-labeled (trace-marker) leaves in a tree.

Equations

• t.traceLeafCount = RoseTree.leafCountP (fun (x : α ⊕ β) => x.isRight = true) t

def RoseTree.traceDepthSum {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : ℕ

Sum of root-distances of the Sum.inr-labeled (trace-marker) leaves.

Equations

• t.traceDepthSum = RoseTree.leafDepthSumP (fun (x : α ⊕ β) => x.isRight = true) t

@[simp]

theorem RoseTree.traceLeafCount_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (node (Sum.inr b) []).traceLeafCount = 1

@[simp]

theorem RoseTree.traceLeafCount_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (node (Sum.inl a) []).traceLeafCount = 0

theorem RoseTree.traceLeafCount_node_of_ne_nil {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) (h : cs ≠ []) : (node v cs).traceLeafCount = (List.map traceLeafCount cs).sum

@[simp]

theorem RoseTree.traceLeafCount_node_cons {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (c : RoseTree (α ⊕ β)) (cs : List (RoseTree (α ⊕ β))) : (node v (c :: cs)).traceLeafCount = (List.map traceLeafCount (c :: cs)).sum

@[simp]

theorem RoseTree.traceLeafCount_node_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount = (List.map traceLeafCount cs).sum

@[simp]

theorem RoseTree.traceDepthSum_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (node (Sum.inl a) []).traceDepthSum = 0

@[simp]

theorem RoseTree.traceDepthSum_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (node (Sum.inr b) []).traceDepthSum = 0

@[simp]

theorem RoseTree.traceDepthSum_node {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : (node v cs).traceDepthSum = (List.map (fun (c : RoseTree (α ⊕ β)) => c.traceDepthSum + c.traceLeafCount) cs).sum

theorem RoseTree.traceLeafCount_perm {α : Type u_1} {β : Type u_2} {t s : RoseTree (α ⊕ β)} (h : t.Perm s) : t.traceLeafCount = s.traceLeafCount

theorem RoseTree.traceDepthSum_perm {α : Type u_1} {β : Type u_2} {t s : RoseTree (α ⊕ β)} (h : t.Perm s) : t.traceDepthSum = s.traceDepthSum

theorem RoseTree.traceLeafCount_le_node {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : (List.map traceLeafCount cs).sum ≤ (node v cs).traceLeafCount

theorem RoseTree.traceLeafCount_le_numNodes {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : t.traceLeafCount ≤ t.numNodes

theorem RoseTree.traceLeafCount_lt_numNodes_of_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount < (node (Sum.inl a) cs).numNodes

theorem RoseTree.traceLeafCount_le_traceDepthSum_of_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount ≤ (node (Sum.inl a) cs).traceDepthSum

def UnorderedTree.traceLeafCount {α : Type u_1} {β : Type u_2} : UnorderedTree (α ⊕ β) → ℕ

The number of Sum.inr-labeled (trace-marker) leaves of a nonplanar tree.

Equations

• UnorderedTree.traceLeafCount = UnorderedTree.leafCountP fun (x : α ⊕ β) => x.isRight = true

@[simp]

theorem UnorderedTree.traceLeafCount_mk {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : (mk t).traceLeafCount = t.traceLeafCount

@[simp]

theorem UnorderedTree.traceLeafCount_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (leaf (Sum.inl a)).traceLeafCount = 0

@[simp]

theorem UnorderedTree.traceLeafCount_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (leaf (Sum.inr b)).traceLeafCount = 1

@[simp]

theorem UnorderedTree.traceLeafCount_node_inl {α : Type u_1} {β : Type u_2} (a : α) (F : Multiset (UnorderedTree (α ⊕ β))) : (node (Sum.inl a) F).traceLeafCount = (Multiset.map traceLeafCount F).sum

def UnorderedTree.traceDepthSum {α : Type u_1} {β : Type u_2} : UnorderedTree (α ⊕ β) → ℕ

The depth-weighted trace-marker count of a nonplanar tree.

Equations

• UnorderedTree.traceDepthSum = UnorderedTree.leafDepthSumP fun (x : α ⊕ β) => x.isRight = true

@[simp]

theorem UnorderedTree.traceDepthSum_mk {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : (mk t).traceDepthSum = t.traceDepthSum

@[simp]

theorem UnorderedTree.traceDepthSum_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (leaf (Sum.inl a)).traceDepthSum = 0

@[simp]

theorem UnorderedTree.traceDepthSum_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (leaf (Sum.inr b)).traceDepthSum = 0

@[simp]

theorem UnorderedTree.traceDepthSum_node_inl {α : Type u_1} {β : Type u_2} (a : α) (F : Multiset (UnorderedTree (α ⊕ β))) : (node (Sum.inl a) F).traceDepthSum = (Multiset.map (fun (c : UnorderedTree (α ⊕ β)) => c.traceDepthSum + c.traceLeafCount) F).sum

theorem UnorderedTree.traceLeafCount_lt_numNodes_of_rootInl {α : Type u_1} {β : Type u_2} (t : UnorderedTree (α ⊕ β)) (x : α) (h : t.rootValue = Sum.inl x) : t.traceLeafCount < t.numNodes

theorem UnorderedTree.traceLeafCount_le_traceDepthSum_of_rootInl {α : Type u_1} {β : Type u_2} (t : UnorderedTree (α ⊕ β)) (x : α) (h : t.rootValue = Sum.inl x) : t.traceLeafCount ≤ t.traceDepthSum

Tree-level trace-leaf conservation

theorem ConnesKreimer.cutSummandsG_traceLeafCount {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (hext : ∀ (t : RoseTree (α ⊕ β)) (r : List (RoseTree (α ⊕ β))), extract t = some r → (List.map RoseTree.traceLeafCount r).sum = 1) (t : RoseTree (α ⊕ β)) (p : Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β)) : p ∈ cutSummandsG extract t → (Multiset.map RoseTree.traceLeafCount p.1).sum + p.2.traceLeafCount = t.traceLeafCount + p.1.card

Trace-leaf conservation for Δ^c cut summands (tree level): each contraction replaces an extracted subtree by one Sum.inr leaf, so crown trace leaves plus trunk trace leaves recover the tree's trace leaves plus one per cut. Requires unit-trace-count replacements.

theorem ConnesKreimer.cutListSummandsG_traceLeafCount {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (hext : ∀ (t : RoseTree (α ⊕ β)) (r : List (RoseTree (α ⊕ β))), extract t = some r → (List.map RoseTree.traceLeafCount r).sum = 1) (cs : List (RoseTree (α ⊕ β))) (q : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : q ∈ cutListSummandsG extract cs → (Multiset.map RoseTree.traceLeafCount q.1).sum + (List.map RoseTree.traceLeafCount q.2).sum = (List.map RoseTree.traceLeafCount cs).sum + q.1.card

Mutual aux: trace-leaf conservation for children-list cut summands.

theorem ConnesKreimer.augActionG_traceLeafCount {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (hext : ∀ (t : RoseTree (α ⊕ β)) (r : List (RoseTree (α ⊕ β))), extract t = some r → (List.map RoseTree.traceLeafCount r).sum = 1) (t : RoseTree (α ⊕ β)) (a : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : a ∈ augActionG extract t → (Multiset.map RoseTree.traceLeafCount a.1).sum + (List.map RoseTree.traceLeafCount a.2).sum = t.traceLeafCount + a.1.card

Mutual aux: trace-leaf conservation for per-child actions.

theorem ConnesKreimer.cutSummandsG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (p : Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β)) : p ∈ cutSummandsG extract t → (Multiset.map RoseTree.traceLeafCount p.1).sum ≤ t.traceLeafCount

Crown trace leaves are bounded by the source's (tree level): the extracted crown forest of any cut has no more trace leaves than the whole tree, since each crown component is a subtree. Independent of the replacement policy (no hext hypothesis) — only the crown side is counted. Together with cutSummandsG_traceLeafCount this forces ≥ 1 fresh trace per cut into the trunk (cutSummandsCN_trunk_traceLeafCount_ge_card).

theorem ConnesKreimer.cutListSummandsG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (cs : List (RoseTree (α ⊕ β))) (q : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : q ∈ cutListSummandsG extract cs → (Multiset.map RoseTree.traceLeafCount q.1).sum ≤ (List.map RoseTree.traceLeafCount cs).sum

Mutual aux: crown trace-leaf bound for children-list cut summands.

theorem ConnesKreimer.augActionG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (a : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : a ∈ augActionG extract t → (Multiset.map RoseTree.traceLeafCount a.1).sum ≤ t.traceLeafCount

Mutual aux: crown trace-leaf bound for per-child actions.

UnorderedTree descent

theorem ConnesKreimer.cutSummandsCN_traceLeafCount {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map UnorderedTree.traceLeafCount p.1).sum + p.2.traceLeafCount = T.traceLeafCount + p.1.card

Trace-leaf conservation for the nonplanar Δ^c cuts: each contraction adds exactly one Sum.inr leaf to the trunk (MCB Lemma 1.6.3).

theorem ConnesKreimer.cutSummandsCN_numNodes {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map UnorderedTree.numNodes p.1).sum + p.2.numNodes = T.numNodes + p.1.card

Weight (vertex) conservation for the nonplanar Δ^c cuts: crown vertices plus trunk vertices recover the tree vertices plus one replacement trace leaf per cut (MCB Lemma 1.6.3).

def ConnesKreimer.Cut.numContractions {α : Type u_3} {β : Type u_4} (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℕ

The number of contractions in a Δ^c cut summand: one per extracted crown component (MCB; numContractions in the legacy AdmissibleCut).

Equations

• ConnesKreimer.Cut.numContractions p = p.1.card

def ConnesKreimer.Cut.depthC {α : Type u_3} {β : Type u_4} (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℕ

The Minimal-Search depth of a Δ^c cut summand (MCB §1.5.2): the total extraction depth Σ d_{v_i}, read off the trunk's trace markers. The Δ^c quotient places a trace leaf at each cut site at exactly the cut depth, so the trunk's traceDepthSum is the signed +d extraction cost of MCB rule 1. Under Internal Merge the matching −d quotient term (rule 2) references this same value and cancels it (cost 0); Sideward Merge incurs it uncancelled (cost > 0, Cut.depthC_pos). Depends only on the trunk p.2, like Cut.numContractions depends only on the crown.

Equations

• ConnesKreimer.Cut.depthC p = p.2.traceDepthSum

theorem ConnesKreimer.cutSummandsCN_lexical_conservation {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map UnorderedTree.traceLeafCount p.1).sum + p.2.traceLeafCount + T.numNodes = (Multiset.map UnorderedTree.numNodes p.1).sum + p.2.numNodes + T.traceLeafCount

Lexical (non-trace) vertex conservation: combining weight and trace-leaf conservation, the trace leaf added at each cut is excluded from the lexical count exactly when the vertex it replaced is removed, so non-trace vertices are conserved with no correction term. Stated additively to avoid truncated ℕ subtraction.

theorem ConnesKreimer.cutSummandsCN_crown_traceLeafCount_le {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map UnorderedTree.traceLeafCount p.1).sum ≤ T.traceLeafCount

Crown trace leaves bounded by the source's, descended to UnorderedTree: the extracted crown forest of a Δ^c cut has no more trace markers than T. (Each crown component is a subtree of T.)

theorem ConnesKreimer.cutSummandsCN_trunk_traceLeafCount_ge_card {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.1.card ≤ p.2.traceLeafCount

Each Δ^c contraction leaves ≥ 1 trace marker in the trunk (MCB Lemma 1.6.3 corollary): the trunk's trace count is at least the number of cuts. From trace-leaf conservation (Σtrace(crown) + trace(trunk) = trace(T) + #cuts) and the crown bound (Σtrace(crown) ≤ trace(T)).

Crown components are policy-chosen (non-degeneracy substrate)

theorem ConnesKreimer.cutSummandsG_crown_isSome {α : Type u_3} {β : Type u_4} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (p : Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β)) : p ∈ cutSummandsG extract t → ∀ (Tv : RoseTree (α ⊕ β)), Tv ∈ p.1 → extract Tv ≠ none

Every crown component of a cut is one the policy chose to extract.

theorem ConnesKreimer.cutListSummandsG_crown_isSome {α : Type u_3} {β : Type u_4} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (cs : List (RoseTree (α ⊕ β))) (q : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : q ∈ cutListSummandsG extract cs → ∀ (Tv : RoseTree (α ⊕ β)), Tv ∈ q.1 → extract Tv ≠ none

theorem ConnesKreimer.augActionG_crown_isSome {α : Type u_3} {β : Type u_4} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (a : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) : a ∈ augActionG extract t → ∀ (Tv : RoseTree (α ⊕ β)), Tv ∈ a.1 → extract Tv ≠ none

theorem ConnesKreimer.extractC_ne_none_imp_inl {α : Type u_3} {β : Type u_4} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (h : extractC τ t ≠ none) : ∃ (a : α), ∃ (cs : List (RoseTree (α ⊕ β))), t = RoseTree.node (Sum.inl a) cs

The Δ^c policy extracts only Sum.inl-rooted (lexical) subtrees.

theorem ConnesKreimer.cutSummandsCN_crown_traceLeafCount_lt_numNodes {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → ∀ (Tv : UnorderedTree (α ⊕ β)), Tv ∈ p.1 → Tv.traceLeafCount < Tv.numNodes

Crown components of a Δ^c cut are lexical-rooted, hence have strictly more vertices than trace leaves.

theorem ConnesKreimer.cutSummandsCN_trunk_rootValue {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.2.rootValue = T.rootValue

A Δ^c cut never touches the root: the trunk keeps the tree's root label.

Minimal-Search depth of a proper cut

theorem ConnesKreimer.Cut.depthC_pos {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (hproper : p.1 ≠ 0) : 1 ≤ depthC p

A proper Δ^c cut of a lexical-rooted tree has trunk trace-depth at least one: the trunk keeps the lexical root, so each of its fresh trace markers sits at depth at least one.

Vertex conservation for the deletion cuts

The deletion cut enumeration cutSummandsP extracts a crown forest and removes the cut subtrees entirely, with no trace placeholder, so vertices are conserved exactly and without a +#cuts correction. Rebinarizing the remainder with contractUnary drops one vertex per contracted unary node, which is the +2 per cut in the edge count of a single deletion.

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

Vertex conservation for the deletion cuts of a tree: crown vertices plus trunk vertices recover the tree's vertices exactly.

theorem ConnesKreimer.cutListSummandsP_numNodes {α : Type u_3} (cs : List (RoseTree α)) (q : Multiset (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

Vertex conservation for the deletion cuts of a list of children.

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

Vertex conservation for the per-child deletion actions.

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

Vertex conservation for the nonplanar deletion cuts.

theorem ConnesKreimer.cutSummandsN_crown_ne_singleton {α : Type u_3} (T : UnorderedTree α) (p : Multiset (UnorderedTree α) × UnorderedTree α) (hp : p ∈ cutSummandsN T) : p.1 ≠ {T}

No deletion cut extracts the whole tree as its crown; the full-tree extraction is the separate primitive term of the coproduct.

theorem ConnesKreimer.cutSummandsN_self_not_mem_crown {α : Type u_3} (T : UnorderedTree α) (p : Multiset (UnorderedTree α) × UnorderedTree α) (hp : p ∈ cutSummandsN T) : ¬T ∈ p.1

No deletion cut of T has T itself among its crown components.

theorem ConnesKreimer.cutSummandsN_numEdges_single_deletion {α : Type u_3} (T : UnorderedTree α) (p : Multiset (UnorderedTree α) × UnorderedTree α) (hp : p ∈ cutSummandsN T) (mover : UnorderedTree α) (hcard : p.1 = {mover}) (huc : p.2.numUnary = 1) : T.numEdges = mover.numEdges + p.2.contractUnary.numEdges + 2

Deleting one subtree mover and rebinarizing the remainder removes two edges: the subtree's own edge and the contracted parent. numUnary p.2 = 1 says the cut was a single edge at a binary node.