Docs / Syntax / Minimalist / Workspace / NoComplexityLoss
import Linglib.Syntax.Minimalist.Workspace.NoComplexityLoss · namespace Minimalist
No Complexity Loss is a condition on a transformation F → F' of workspaces (Definition 1.6.2 of
Marcolli, Chomsky and Berwick): the map sending each component of F to the component of F'
holding its root never decreases degree, so Merge builds hierarchical structure of nondecreasing
complexity. NoComplexityLoss.Map deg φ checks a component map, as a multiset φ of pairs, for
a degree deg, and NoComplexityLoss deg F F' asks for one from F to F'.
A term of Merge chooses a cut for each component, so its own map, componentMap, sends a
component taken whole to the Merge and a cut component to its trunk. Along it, no complexity is
lost exactly when every component is taken whole or left uncut, as External Merge does. Every
Sideward term, and every term of the unit stage on its own, cuts a component and loses complexity
(Proposition 1.6.10). These hold for any positive degree whose cuts have a fixed extraction
cost.
The book grades by leaf count. A degree that each cut conserves avoids the nullary-node
corrections leaf count incurs when a node loses all its children under a multi-edge cut. At the
pruning cuts this is the vertex count, the canonical Connes–Kreimer grading. At the trace cuts a
trace leaf takes the place of each extracted tree, so extracting a single lexical item keeps the
vertex count. They conserve instead the size σ, which leaves trace leaves out (the book's
(1.6.10)), and graded by σ every Sideward term loses complexity there too.
Minimalist.NoComplexityLoss, Minimalist.NoComplexityLoss.MapMinimalist.componentMap: the component map of a choice of cuts.Minimalist.NoComplexityLoss.of_componentMap: the component map of a term of Merge goes to the
workspace the term builds.Minimalist.NoComplexityLoss.map_componentMap_merge_iff: a term of Merge loses no complexity
exactly when it takes components whole or leaves them uncut.Minimalist.NoComplexityLoss.not_map_componentMap_merge, not_map_componentMap_unit: every
Sideward term and every term of the unit stage loses complexity.Minimalist.NoComplexityLoss.not_map_accessibleSize_componentMap_merge: at the trace cuts,
graded by σ.Marcolli et al. 2025 Definition 1.6.2 states No Complexity Loss for the induced map,
which sends each component of the workspace to the component holding its root afterwards. A term
of Merge or of its unit stage is a choice of a cut for each component (mergeOpG_apply_of'_eq_sum,
mergeOpUnitG_apply_of'_eq_sum), so its induced map pairs a component taken whole with the object
built from the crown, and a cut component with its trunk. As a multiset of pairs it keeps apart
equal components that go to different places.
The results hold for any positive degree with a fixed extraction cost
(CutChoice.HasExtractionCost), such as the degrees each cut conserves: the vertex count at the
pruning cuts (hasExtractionCost_numNodes_cutSummandsN) and the size σ at the trace cuts
(hasExtractionCost_accessibleSize_cutSummandsCN, the book's (1.6.10)).
No Complexity Loss holds along a component map when no component is paired with one of lower degree.
Used by NoComplexityLoss, NoComplexityLoss.of_componentMap, NoComplexityLoss.map_componentMap_iff, NoComplexityLoss.not_map_componentMap, NoComplexityLoss.map_componentMap_merge_iff, NoComplexityLoss.not_map_componentMap_merge, NoComplexityLoss.not_map_componentMap_unit, NoComplexityLoss.not_map_accessibleSize_componentMap_merge
A workspace transformation F → F' satisfies No Complexity Loss when some component map,
pairing each component of F with a component of F', loses no degree
(Marcolli et al. 2025 Definition 1.6.2 asks this of the induced map).
Built from
Used by NoComplexityLoss.of_componentMap
The component map of a choice of cuts sends a tree taken whole to the object X built from the
crown, and a cut tree to its trunk.
The definition is too large to print here; read it in the source.
Used by NoComplexityLoss.of_componentMap, NoComplexityLoss.map_componentMap_iff, NoComplexityLoss.not_map_componentMap, NoComplexityLoss.map_componentMap_merge_iff, NoComplexityLoss.not_map_componentMap_merge, NoComplexityLoss.not_map_componentMap_unit, NoComplexityLoss.not_map_accessibleSize_componentMap_merge
The component map of a term of Merge pairs each component of the workspace with a component of the workspace the term builds.
Built from , ,
Along the component map of a choice of cuts with an extraction cost in a positive degree, no
complexity is lost exactly when every tree is taken whole or left uncut, provided the object
X outweighs the trees taken whole.
Built from ,
A tree of the crown that is not a component of the workspace was cut out of a component, and that component goes to a trunk of lower degree.
Built from ,
A term of Merge loses no complexity along its component map exactly when it takes trees whole or leaves them uncut (Marcolli et al. 2025 Proposition 1.6.10).
Built from ,
Every term of Sideward Merge loses complexity along its component map (Marcolli et al. 2025 Proposition 1.6.10).
Built from ,
Every term of the unit stage M_{β,1} with β not a component of the workspace loses
complexity along its component map (Marcolli et al. 2025 Proposition 1.6.10).
Built from ,
Graded by vertices, a term of Merge at the trace cuts may lose nothing, since a trace leaf takes
the place of each extracted tree. Graded by the size σ, which the trace cuts conserve, every
Sideward term loses complexity.
At the trace cuts, graded by the size σ, every term of Sideward Merge loses complexity along
its component map (Marcolli et al. 2025 Proposition 1.6.10).
Built from ,