Trace-aware size measures of workspaces

A workspace F on the carrier UnorderedTree (α ⊕ β), with Sum.inr marking a trace, is measured by its number of components Multiset.card F, its number of accessible terms, which are the non-root vertices Forest.numEdges F, and its number of vertices Forest.numNodes F = card F + numEdges F. Under the trace-preserving coproduct a cut leaves a trace leaf that is not an accessible term, so the trace-aware count discounts trace leaves: accessibleCount T = numEdges T − traceLeafCount T on a tree, summed over a forest, and accessibleSize F = card F + accessibleCount F. The extraction identities say how a Δ^c cut of a lexical-rooted object splits its accessible terms between crown and trunk, one contraction per cut.

Main definitions

• UnorderedTree.accessibleCount, Forest.accessibleCount, Forest.accessibleSize

Main results

• ConnesKreimer.cutSummandsCN_accessibleCount_single, _pair: the extraction identities.

References

• [marcolli-chomsky-berwick-2025], §1.6.1–1.6.2 (Lemma 1.6.3)

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

accessibleCount T = numEdges T − traceLeafCount T, the accessible terms of T that are not traces.

Equations

• t.accessibleCount = t.numEdges - t.traceLeafCount

@[simp]

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

@[simp]

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

theorem UnorderedTree.accessibleCount_merge {α : Type u_1} {β : Type u_2} (a : α) (l r : UnorderedTree (α ⊕ β)) (hl : l.traceLeafCount < l.numNodes) (hr : r.traceLeafCount < r.numNodes) : (node (Sum.inl a) {l, r}).accessibleCount = l.accessibleCount + r.accessibleCount + 2

External Merge adds two accessible terms.

def Forest.accessibleCount {α : Type u_1} {β : Type u_2} (F : Multiset (UnorderedTree (α ⊕ β))) : ℕ

The accessible terms of a workspace that are not traces, summed over its components.

Equations

• Forest.accessibleCount F = (Multiset.map UnorderedTree.accessibleCount F).sum

@[simp]

theorem Forest.accessibleCount_zero {α : Type u_1} {β : Type u_2} : accessibleCount 0 = 0

@[simp]

theorem Forest.accessibleCount_cons {α : Type u_1} {β : Type u_2} (T : UnorderedTree (α ⊕ β)) (F : Multiset (UnorderedTree (α ⊕ β))) : accessibleCount (T ::ₘ F) = T.accessibleCount + accessibleCount F

@[simp]

theorem Forest.accessibleCount_singleton {α : Type u_1} {β : Type u_2} (T : UnorderedTree (α ⊕ β)) : accessibleCount {T} = T.accessibleCount

@[simp]

theorem Forest.accessibleCount_add {α : Type u_1} {β : Type u_2} (F G : Multiset (UnorderedTree (α ⊕ β))) : accessibleCount (F + G) = accessibleCount F + accessibleCount G

def Forest.accessibleSize {α : Type u_1} {β : Type u_2} (F : Multiset (UnorderedTree (α ⊕ β))) : ℕ

accessibleSize F = card F + accessibleCount F, the trace-aware size of a workspace.

Equations

• Forest.accessibleSize F = F.card + Forest.accessibleCount F

@[simp]

theorem Forest.accessibleSize_zero {α : Type u_1} {β : Type u_2} : accessibleSize 0 = 0

@[simp]

theorem Forest.accessibleSize_cons {α : Type u_1} {β : Type u_2} (T : UnorderedTree (α ⊕ β)) (F : Multiset (UnorderedTree (α ⊕ β))) : accessibleSize (T ::ₘ F) = T.accessibleCount + 1 + accessibleSize F

@[simp]

theorem Forest.accessibleSize_singleton {α : Type u_1} {β : Type u_2} (T : UnorderedTree (α ⊕ β)) : accessibleSize {T} = T.accessibleCount + 1

@[simp]

theorem Forest.accessibleSize_add {α : Type u_1} {β : Type u_2} (F G : Multiset (UnorderedTree (α ⊕ β))) : accessibleSize (F + G) = accessibleSize F + accessibleSize G

theorem ConnesKreimer.cutSummandsCN_accessibleCount_single {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (F₀ : Multiset (UnorderedTree (α ⊕ β))) (hT : T = UnorderedTree.node (Sum.inl a₀) F₀) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (Tv : UnorderedTree (α ⊕ β)) (hcard : p.1 = {Tv}) : T.accessibleCount = Tv.accessibleCount + p.2.accessibleCount + 1

Contracting one accessible subtree Tv out of a lexical-rooted object splits its accessible terms as accessibleCount T = accessibleCount Tv + accessibleCount (T/Tv) + 1, the +1 being the contraction itself.

theorem ConnesKreimer.cutSummandsCN_accessibleCount_pair {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (F₀ : Multiset (UnorderedTree (α ⊕ β))) (hT : T = UnorderedTree.node (Sum.inl a₀) F₀) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ cutSummandsCN τ T) (Tv Tw : UnorderedTree (α ⊕ β)) (hcard : p.1 = {Tv, Tw}) : T.accessibleCount = Tv.accessibleCount + Tw.accessibleCount + p.2.accessibleCount + 2

Contracting two accessible subtrees adds two contractions: accessibleCount T is accessibleCount Tv + accessibleCount Tw + accessibleCount (T/{Tv,Tw}) + 2.