Vertex conservation for pruning cuts

A pruning cut removes its crown subtrees entirely, so crown vertices and trunk vertices recover the vertices of the tree exactly. Hence every crown component, and the trunk of a proper cut, is smaller than the tree: the descent that makes recursions over cuts, such as the antipode, well founded. Contracting the vertices the cut leaves with a single child then removes one more vertex for each.

Main results

• ConnesKreimer.cutSummandsN_numNodes, hasExtractionCost_numNodes_cutSummandsN: vertex conservation for the nonplanar pruning cuts, and for a choice of them over a forest.
• ConnesKreimer.cutSummandsN_crown_numNodes_lt, ConnesKreimer.cutSummandsN_trunk_numNodes_lt: crowns and proper trunks are smaller than the tree.
• ConnesKreimer.cutSummandsN_numEdges_contractUnary: the edges of the tree, of the crown and of the contracted trunk.
• ConnesKreimer.cutSummandsN_numUnary: in a full binary tree a cut leaves a unary vertex for each tree it extracts, less two for each vertex both of whose children it extracts.

References

• [CK98]

Vertex conservation for the pruning cuts

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

The crown and the trunk of a pruning cut have exactly the vertices of the tree.

theorem ConnesKreimer.hasExtractionCost_numNodes_cutSummandsN {α : Type u_1} {F : Multiset (UnorderedTree α)} {s : CutChoice α} (hs : s ∈ forestCutChoicesG cutSummandsN F) : CutChoice.HasExtractionCost UnorderedTree.numNodes 0 s

A choice of pruning cuts conserves vertices.

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

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

theorem ConnesKreimer.cutSummandsN_crown_numNodes_lt {α : Type u_1} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hp : p ∈ cutSummandsN T) {t : UnorderedTree α} (ht : t ∈ p.1) : t.numNodes < T.numNodes

Every crown component of a pruning cut has fewer vertices than the tree.

theorem ConnesKreimer.cutSummandsN_trunk_numNodes_lt {α : Type u_1} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hp : p ∈ cutSummandsN T) (h : p.1 ≠ 0) : p.2.numNodes < T.numNodes

The trunk of a pruning cut with a nonempty crown has fewer vertices than the tree.

theorem ConnesKreimer.cutSummandsN_crown_numEdges_lt {α : Type u_1} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hp : p ∈ cutSummandsN T) (h : p.1 ≠ 0) : (Multiset.map UnorderedTree.numEdges p.1).sum < T.numEdges

A nonempty crown of a pruning cut has fewer edges in total than the tree.

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

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

Unary vertices left by a pruning cut

The deletion coproduct contracts the vertices a pruning cut leaves with a single child. In a full binary tree the cut leaves the parent of each tree it extracts with a single child, unless it extracts both of the parent's children, which leaves the parent a leaf.

theorem ConnesKreimer.cutSummandsN_numEdges_contractUnary {α : Type u_1} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hp : p ∈ cutSummandsN T) : T.numEdges = (Multiset.map UnorderedTree.numEdges p.1).sum + p.2.contractUnary.numEdges + p.1.card + p.2.numUnary

Deleting the crown of a pruning cut and contracting the unary vertices of its trunk removes, besides the crown's own edges, one edge for each crown component and one for each unary vertex.

theorem ConnesKreimer.cutSummandsN_numUnary {α : Type u_1} {T : UnorderedTree α} (hT : T.IsFullBinary) {p : Multiset (UnorderedTree α) × UnorderedTree α} (hp : p ∈ cutSummandsN T) : ∃ (k : ℕ), p.1.card = p.2.numUnary + 2 * k

In a full binary tree a pruning cut leaves a unary vertex for each tree it extracts, less two for each vertex both of whose children it extracts.