Docs / Syntax / Minimalist / Workspace / TraceMeasures

Trace-aware size measures of workspaces

import Linglib.Syntax.Minimalist.Workspace.TraceMeasures

Source

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 (F.map UnorderedTree.numEdges).sum, and its number of vertices, the summed numNodes, which is card F plus the summed numEdges. 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 − numTraces 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

Main results

References

Declarations

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

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

Used by UnorderedTree.accessibleCount_leaf_inl, UnorderedTree.accessibleCount_leaf_inr, UnorderedTree.accessibleCount_merge, Forest.accessibleCount, Forest.accessibleCount_cons, Forest.accessibleCount_singleton, Forest.accessibleSize_cons, Forest.accessibleSize_singleton, ConnesKreimer.cutSummandsCN_accessibleCount, ConnesKreimer.accessibleCount_merge_of_crown_eq, ConnesKreimer.hasExtractionCost_accessibleCount_cutSummandsCN

Used in Syntax/Minimalist/Workspace/Derivation, Syntax/Minimalist/Workspace/MinimalYield, KitaharaSeely2026, MarcolliChomskyBerwick2025

L52–53
L55–56

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

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

Built from

Used by Forest.accessibleCount_zero, Forest.accessibleCount_cons, Forest.accessibleCount_singleton, Forest.accessibleCount_add, Forest.accessibleSize

Used in Syntax/Minimalist/Workspace/MinimalYield

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

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

Built from

Used by Forest.accessibleSize_zero, Forest.accessibleSize_cons, Forest.accessibleSize_singleton, Forest.accessibleSize_add, ConnesKreimer.cutSummandsCN_accessibleSize, ConnesKreimer.hasExtractionCost_accessibleSize_cutSummandsCN

Used in Syntax/Minimalist/Workspace/Derivation, Syntax/Minimalist/Workspace/MinimalYield, Syntax/Minimalist/Workspace/NoComplexityLoss

accessibleCount T is the crown's and the trunk's accessible terms plus one per tree extracted by a Δ^c cut (Marcolli et al. 2025 (1.6.8)).

theorem ConnesKreimer.cutSummandsCN_accessibleCountL135–152
{α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) {T : UnorderedTree (α ⊕ β)} (hT : T.value.isLeft = true) {p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} (hp : p ∈ cutSummandsCN τ T) :
T.accessibleCount = (Multiset.map UnorderedTree.accessibleCount p.1).sum + p.2.accessibleCount + p.1.card

Built from

A Δ^c cut of a lexical-rooted object splits its size σ exactly between its crown and its trunk (Marcolli et al. 2025 (1.6.10)).

theorem ConnesKreimer.cutSummandsCN_accessibleSizeL154–164
{α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) {T : UnorderedTree (α ⊕ β)} (hT : T.value.isLeft = true) {p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} (hp : p ∈ cutSummandsCN τ T) :
(Multiset.map (fun (c : UnorderedTree (α ⊕ β)) => Forest.accessibleSize {c}) p.1).sum + Forest.accessibleSize {p.2} = Forest.accessibleSize {T}

Built from

L183–195

A choice of trace cuts costs one accessible term for each tree it extracts, when the trees it cuts or takes whole are not traces.

theorem ConnesKreimer.hasExtractionCost_accessibleCount_cutSummandsCNL197–210
{α : Type u_1} {β : Type u_2} {τ : UnorderedTree (α ⊕ β) → β} {F : Multiset (UnorderedTree (α ⊕ β))} {s : CutChoice (α ⊕ β)} (hs : s ∈ forestCutChoicesG (cutSummandsCN τ) F) (hF : ∀ x ∈ s, x.2.1 ≠ 0 → x.1.value.isLeft = true) :
CutChoice.HasExtractionCost UnorderedTree.accessibleCount 1 s

Built from

A choice of trace cuts conserves the size σ, when the trees it cuts or takes whole are not traces.

theorem ConnesKreimer.hasExtractionCost_accessibleSize_cutSummandsCNL212–225
{α : Type u_1} {β : Type u_2} {τ : UnorderedTree (α ⊕ β) → β} {F : Multiset (UnorderedTree (α ⊕ β))} {s : CutChoice (α ⊕ β)} (hs : s ∈ forestCutChoicesG (cutSummandsCN τ) F) (hF : ∀ x ∈ s, x.2.1 ≠ 0 → x.1.value.isLeft = true) :
CutChoice.HasExtractionCost (fun (T : UnorderedTree (α ⊕ β)) => Forest.accessibleSize {T}) 0 s

Built from