Conservation laws for the Δ^c (contraction) cut enumeration

[MCB25]

Size bookkeeping for the trace-preserving admissible-cut coproduct cutSummandsCN on Nonplanar (α ⊕ β). A cut summand p = (p.1, p.2) splits a syntactic object into a crown forest p.1 (the extracted subtrees) and a trunk p.2 (the contraction quotient, carrying one trace-marker leaf per cut). The two primitive conservation laws are:

• weight (cutSummandsCN_numNodes): Σ #V(crown) + #V(trunk) = #V(T) + #cuts — extracting a subtree removes its vertices but leaves one replacement trace leaf per cut.
• trace leaves (cutSummandsCN_traceLeafCount): Σ #trace(crown) + #trace(trunk) = #trace(T) + #cuts — each contraction adds exactly one Sum.inr leaf.

Combined, they give exact conservation of lexical (non-trace) vertices (cutSummandsCN_lexical_conservation): the trace leaf added at each cut is excluded from the lexical count, cancelling the vertex it replaces. These are MCB's Lemma 1.6.3 conservation laws on the canonical carrier; the legacy planar-binary forms were AdmissibleCut.cut_size_conservation and cut_leafCount_conservation.

Main results

• ConnesKreimer.cutSummandsG_traceLeafCount — trace-leaf conservation at the planar level (mutual with the list/per-child auxiliaries).
• cutSummandsCN_traceLeafCount, cutSummandsCN_numNodes — descended to Nonplanar.
• cutSummandsCN_lexical_conservation — exact non-trace-vertex conservation.
• Cut.numContractions — #cuts = card of the crown forest.

TODO

• The accessible-term / α extraction identities in accCount/accCountC form (MCB eq. 1.6.8 α(T) = α(Tv) + αᶜ(trunk) + 1 for a single cut, and the σ-forms 1.6.9/1.6.10) — corollaries of the two conservation laws, modulo truncated-ℕ positivity bookkeeping.

Tree-level trace-leaf conservation

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

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

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

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

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

theorem RootedTree.ConnesKreimer.cutSummandsG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (p : Forest (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 RootedTree.ConnesKreimer.cutListSummandsG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (cs : List (RoseTree (α ⊕ β))) (q : Forest (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 RootedTree.ConnesKreimer.augActionG_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (extract : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))) (t : RoseTree (α ⊕ β)) (a : Forest (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.

Nonplanar descent

theorem RootedTree.cutSummandsCN_traceLeafCount {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map Nonplanar.traceLeafCount p.1).sum + p.2.traceLeafCount = T.traceLeafCount + Multiset.card p.1

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 RootedTree.cutSummandsCN_numNodes {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map Nonplanar.numNodes p.1).sum + p.2.numNodes = T.numNodes + Multiset.card p.1

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 RootedTree.Cut.numContractions {α : Type u_1} {β : Type u_2} (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : ℕ

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

Equations

• RootedTree.Cut.numContractions p = Multiset.card p.1

def RootedTree.Cut.depthC {α : Type u_1} {β : Type u_2} (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : ℕ

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

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

theorem RootedTree.cutSummandsCN_lexical_conservation {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map Nonplanar.traceLeafCount p.1).sum + p.2.traceLeafCount + T.numNodes = (Multiset.map Nonplanar.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 RootedTree.cutSummandsCN_crown_traceLeafCount_le {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map Nonplanar.traceLeafCount p.1).sum ≤ T.traceLeafCount

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

theorem RootedTree.cutSummandsCN_trunk_traceLeafCount_ge_card {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → Multiset.card p.1 ≤ 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)).

Non-degeneracy: lexical-rooted pieces have a non-trace vertex

The single-cut α extraction identity (eq. 1.6.8) needs that each piece (the extracted subtree, the trunk, the whole tree) has at least one non-trace vertex, so that accCountC = #V − 1 − #trace does not truncate. Crown components are always Sum.inl-rooted (the Δ^c policy declines to cut trace nodes), and the trunk keeps the tree's root.

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

A trace leaf is a vertex, so a tree has at least as many vertices as trace leaves.

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

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

A lexical-rooted tree has a non-trace vertex (its root), so its trace leaves number strictly fewer than its vertices.

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

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

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

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

theorem RootedTree.ConnesKreimer.extractC_ne_none_imp_inl {α : Type u_1} {β : Type u_2} (τ : 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 RootedTree.Nonplanar.traceLeafCount_lt_numNodes_of_rootInl {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) (a : α) (h : t.rootValue = Sum.inl a) : t.traceLeafCount < t.numNodes

A lexical-rooted (Sum.inl) nonplanar tree has a non-trace vertex (its root), so its trace leaves number strictly fewer than its vertices.

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

A lexical-rooted nonplanar tree puts every trace marker at depth ≥ 1, so its depth-weighted trace count dominates its plain trace count.

α extraction identity (MCB eq. 1.6.8)

theorem RootedTree.cutSummandsCN_crown_traceLeafCount_lt_numNodes {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → ∀ 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 RootedTree.cutSummandsCN_trunk_rootValue {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.2.rootValue = T.rootValue

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

theorem RootedTree.cutSummandsCN_accCountC_single {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (a₀ : α) (F₀ : Forest (Nonplanar (α ⊕ β))) (hT : T = Nonplanar.node (Sum.inl a₀) F₀) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (Tv : Nonplanar (α ⊕ β)) (hcard : p.1 = {Tv}) : T.accCountC = Tv.accCountC + p.2.accCountC + 1

Single-cut accessible-term extraction (MCB eq. 1.6.8): contracting one accessible subtree Tv out of a lexical-rooted syntactic object splits its accessible terms as αᶜ(T) = αᶜ(Tv) + αᶜ(T/^c Tv) + 1 — the +1 is the contraction itself. Uses accCountC throughout (the trace placeholder left at the cut site is not an accessible term).

theorem RootedTree.cutSummandsCN_accCountC_pair {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (a₀ : α) (F₀ : Forest (Nonplanar (α ⊕ β))) (hT : T = Nonplanar.node (Sum.inl a₀) F₀) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (Tv Tw : Nonplanar (α ⊕ β)) (hcard : p.1 = {Tv, Tw}) : T.accCountC = Tv.accCountC + Tw.accCountC + p.2.accCountC + 2

Two-cut accessible-term extraction (MCB eq. 1.6.8 for a 2-edge admissible cut): contracting two accessible subtrees Tv, Tw adds two contractions, αᶜ(T) = αᶜ(Tv) + αᶜ(Tw) + αᶜ(T/^c {Tv,Tw}) + 2. Used for Sideward Merge 3(a).

Minimal-Search positivity (MCB Prop 1.5.1, Sideward direction)

theorem RootedTree.Cut.depthC_pos {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (hproper : p.1 ≠ 0) : 1 ≤ depthC p

A proper Δ^c cut of a lexical-rooted object costs ≥ 1 (MCB Prop 1.5.1). The trunk keeps the tree's lexical root (cutSummandsCN_trunk_rootValue), so each of its #cuts ≥ 1 fresh trace markers sits at depth ≥ 1; hence the Minimal-Search depth Cut.depthC p = Σ d_{v_i} ≥ #cuts ≥ 1. This is the uncancelled Sideward cost that vanishes at ε → 0, leaving only the cost-0 External and Internal Merges.

Signed Minimal-Search cost (MCB §1.5.2 rules 1–2)

The cost of a Merge 𝔐(α,β) sums the signed depth-costs of its two operands. An extracted accessible term costs +d (rule 1); a contraction quotient costs −d (rule 2). Internal Merge re-grafts an extracted crown with its own quotient, so the two costs of the same cut cancel; Sideward Merge grafts a crown with a non-matching partner, leaving +d uncancelled.

def RootedTree.Cut.extractionCost {α : Type u_1} {β : Type u_2} (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : ℤ

Extraction cost of a Δ^c cut (MCB rule 1): pulling out the crown costs +d, the cut depth Cut.depthC. Signed (ℤ) so it can cancel the quotient cost under Internal Merge.

Equations

• RootedTree.Cut.extractionCost p = ↑(RootedTree.Cut.depthC p)

def RootedTree.Cut.quotientCost {α : Type u_1} {β : Type u_2} (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : ℤ

Quotient cost of a Δ^c cut (MCB rule 2): the contraction quotient (trunk) costs −d — a deep quotient is close to the whole tree, hence cheap. The negative companion to Cut.extractionCost.

Equations

• RootedTree.Cut.quotientCost p = -↑(RootedTree.Cut.depthC p)

theorem RootedTree.Cut.extractionCost_add_quotientCost {α : Type u_1} {β : Type u_2} (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) : extractionCost p + quotientCost p = 0

Internal Merge cancellation (MCB Prop 1.5.1, IM bullet): re-merging an extracted crown T_v with its OWN quotient T_i/T_v sums the two signed costs of the same cut, (+d) + (−d) = 0 — the cost-0 that survives ε → 0. Derives from the two signed rules, not stipulated.

theorem RootedTree.Cut.extractionCost_pos {α : Type u_1} {β : Type u_2} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (hproper : p.1 ≠ 0) : 0 < extractionCost p

Sideward Merge cost is positive (MCB Prop 1.5.1, Sideward bullets): grafting an extracted crown of a lexical-rooted object with a non-matching partner leaves the +d extraction cost uncancelled (no quotient operand to supply the −d). Vanishes at ε → 0.