Docs / Syntax / Minimalist / Workspace / Coproduct / TraceConservation

Trace statistics of cuts

import Linglib.Syntax.Minimalist.Workspace.Coproduct.TraceConservation

Source

The size bookkeeping of the trace cuts cutSummandsCN of Marcolli, Chomsky and Berwick. A cut contracts each tree it extracts to a leaf labelled by the trace of that tree, so its trunk is the quotient by contraction of their Definition 1.2.4 (p. 30); here a trace is a Sum.inr-labelled leaf. Vertices are then conserved up to one trace per extracted tree, the count in the proof of their Lemma 1.6.3 (p. 65), and edges exactly, which makes the number of edges a grading of Δ^c (their Lemma 1.2.10, p. 37). Traces are conserved up to one per extracted tree.

Main definitions

Main results

References

Declarations

L50–52
L54–56
L58–60

The number of traces of a nonplanar tree, its Sum.inr-labelled leaves.

def UnorderedTree.numTracesL77–78
{α : Type u_1} {β : Type u_2} (t : UnorderedTree (α ⊕ β)) :
ℕ
  • t.numTraces = Multiset.countP (fun (x : α ⊕ β) => x.isRight = true) t.leaves

Used by UnorderedTree.numTraces_mk, UnorderedTree.numTraces_leaf_inl, UnorderedTree.numTraces_leaf_inr, UnorderedTree.numTraces_node_inl, UnorderedTree.numTraces_lt_numNodes_of_isLeft, ConnesKreimer.cutSummandsCN_numTraces, ConnesKreimer.eq_zero_of_mem_cutSummandsCN

Used in Syntax/Minimalist/Workspace/MinimalYield, Syntax/Minimalist/Workspace/TraceMeasures

L83–85
L87–89

Trace conservation for a policy leaving one trace per cut

L136–160

The trace cuts