Trace statistics of cuts

The size bookkeeping of the trace cuts cutSummandsCN of Marcolli, Chomsky and Berwick. A trace is a Sum.inr-labelled leaf; a cut splits a tree into a crown forest and a trunk carrying one trace per cut. Vertices are conserved up to the new traces, traces up to one per cut, and lexical vertices exactly.

Main definitions

• RoseTree.traceLeafCount, UnorderedTree.traceLeafCount: the number of traces.

Main results

• ConnesKreimer.cutSummandsCN_numNodes: crown and trunk vertices recover the tree's vertices plus one trace per cut (Lemma 1.6.3).
• ConnesKreimer.cutSummandsCN_traceLeafCount: traces are conserved up to one per cut.
• ConnesKreimer.cutSummandsCN_lexical_conservation: lexical vertices are conserved exactly.
• ConnesKreimer.cutSummandsCN_crown_numEdges_lt: a nonempty crown has fewer edges than the tree.

References

• [MCB25]

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 = Multiset.countP (fun (x : α ⊕ β) => x.isRight = true) t.leaves

@[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

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

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

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

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

Equations

• t.traceLeafCount = Multiset.countP (fun (x : α ⊕ β) => x.isRight = true) t.leaves

@[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

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

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

Under replacements carrying one trace each, crown traces plus trunk traces recover the tree's traces plus one per cut, since each contraction replaces an extracted subtree by one Sum.inr leaf.

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

Trace-leaf conservation for the cut summands of a children list.

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

Trace-leaf conservation for the 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. 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

The crown trace-leaf bound for the cut summands of a children list.

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

The crown trace-leaf bound for the 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

Traces are conserved by the nonplanar Δ^c cuts up to one per cut, since each contraction adds exactly one Sum.inr leaf to the trunk.

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

Vertices are conserved by the nonplanar Δ^c cuts up to traces. Crown vertices plus trunk vertices recover the tree vertices plus one replacement trace leaf per cut (MCB Lemma 1.6.3).

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

Non-trace vertices are conserved exactly by the Δ^c cuts, since the trace leaf added at each cut replaces the root of the extracted subtree. 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

The crown of a Δ^c cut has no more traces than the tree, each crown component being a subtree of it.

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

The trunk of a Δ^c cut has at least one trace per cut, by trace conservation and the crown bound.

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 ∈ 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 ∈ 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 ∈ 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 ∈ 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_value {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.2.value = T.value

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

theorem ConnesKreimer.cutSummandsCN_two_le_trunk_numNodes {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → p.1 ≠ 0 → 2 ≤ p.2.numNodes

A Δ^c cut with a nonempty crown leaves a trunk with at least two vertices, the root and a trace.

theorem ConnesKreimer.cutSummandsCN_crown_numEdges_lt {α : Type u_3} {β : Type u_4} (τ : UnorderedTree (α ⊕ β) → β) {T : UnorderedTree (α ⊕ β)} {p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} (hp : p ∈ cutSummandsCN τ T) (h : p.1 ≠ 0) : (Multiset.map UnorderedTree.numEdges p.1).sum < T.numEdges

A nonempty crown of a Δ^c cut has fewer edges in total than the tree.