Trace-marker measures and conservation laws for the Δ^c cut enumeration

[MCB25]

The trace-marker leaf statistics on RoseTree (α ⊕ β) and Nonplanar (α ⊕ β) (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).

MCB's letter vocabulary over these measures (accCount, αᶜ, σᶜ) and the Merge economy corollaries live in Syntax/Minimalist/Workspace/TraceMeasures.lean and Workspace/Conservation.lean.

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 RoseTree.Nonplanar.traceLeafCount {α : Type u_1} {β : Type u_2} : Nonplanar (α ⊕ β) → ℕ

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem RoseTree.Nonplanar.traceLeafCount_le_traceDepthSum_of_rootInl {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) (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.

Nonplanar descent

theorem ConnesKreimer.cutSummandsCN_traceLeafCount {α : Type u_3} {β : Type u_4} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map RoseTree.Nonplanar.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} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map RoseTree.Nonplanar.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 (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : ℕ

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 (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.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

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

theorem ConnesKreimer.cutSummandsCN_lexical_conservation {α : Type u_3} {β : Type u_4} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map RoseTree.Nonplanar.traceLeafCount p.1).sum + p.2.traceLeafCount + T.numNodes = (Multiset.map RoseTree.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 ConnesKreimer.cutSummandsCN_crown_traceLeafCount_le {α : Type u_3} {β : Type u_4} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map RoseTree.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 ConnesKreimer.cutSummandsCN_trunk_traceLeafCount_ge_card {α : Type u_3} {β : Type u_4} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : 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} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → ∀ (Tv : RoseTree.Nonplanar (α ⊕ β)), 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} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (T : RoseTree.Nonplanar (α ⊕ β)) (p : Multiset (RoseTree.Nonplanar (α ⊕ β)) × RoseTree.Nonplanar (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.2.rootValue = T.rootValue

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