Cuts that leave traces

Marcolli, Chomsky and Berwick's coproduct Δ^c cuts accessible terms out of a syntactic object and leaves a trace in place of each. On trees labelled α ⊕ β, the trace of a cut subtree t is a leaf inr (τ t) whose label is computed by a trace encoder τ, and cuts at trace leaves are forbidden, since a trace is not an accessible term. This is the admissible-cut enumeration cutSummandsG at the extraction policy extractC τ.

Main definitions

• ConnesKreimer.traceLeaf: the trace leaf with a given label.
• ConnesKreimer.extractC: the trace extraction policy.
• ConnesKreimer.cutSummandsCP, ConnesKreimer.cutSummandsCN: the trace cut summands, and their descent to UnorderedTree.

Main results

• ConnesKreimer.cutSummandsCN_numEdges: crown edges plus trunk vertices recover the vertices of the tree.
• ConnesKreimer.cutSummandsCN_filter_empty: the empty cut is the unique cut with empty crown.
• ConnesKreimer.cutSummandsCN_filter_crown_eq_singleton: a lexical subtree occurring once is extracted by one cut, whose trunk replaces it by its trace.

References

• [MCB25]

traceLeaf — placeholder for a cut subtree

def ConnesKreimer.traceLeaf {α : Type u_1} {β : Type u_2} (b : β) : RoseTree (α ⊕ β)

The trace-marker placeholder leaf carrying the encoded label b : β.

Equations

• ConnesKreimer.traceLeaf b = RoseTree.node (Sum.inr b) []

Δ^c extraction policy

def ConnesKreimer.extractC {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))

The Δ^c extraction policy extracts Sum.inl-rooted (non-trace) subtrees whole, leaving a single traceLeaf (τ t) in the parent's child slot, and declines to extract Sum.inr-rooted (trace) subtrees.

Declining at trace subtrees is required for coassociativity — without it, iterated Δ^c produces "trace of trace" right-channel terms that break the double-cut bijection — and matches [MCB25] Definition 1.2.2's restriction of cuts to accessible terms, which excludes trace placeholders.

Equations

• ConnesKreimer.extractC τ (RoseTree.node (Sum.inl val) children) = some [ConnesKreimer.traceLeaf (τ (RoseTree.node (Sum.inl val) children))]
• ConnesKreimer.extractC τ (RoseTree.node (Sum.inr val) children) = none

@[simp]

theorem ConnesKreimer.extractC_inl {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α) (cs : List (RoseTree (α ⊕ β))) : extractC τ (RoseTree.node (Sum.inl a) cs) = some [traceLeaf (τ (RoseTree.node (Sum.inl a) cs))]

@[simp]

theorem ConnesKreimer.extractC_inr {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (b : β) (cs : List (RoseTree (α ⊕ β))) : extractC τ (RoseTree.node (Sum.inr b) cs) = none

cutSummandsCP — Δ^c cut enumeration via the generic cutSummandsG

Defined as cutSummandsG (extractC τ). The generic-side simp lemmas (cutSummandsG_node, cutListSummandsG_*, augActionG_*) compose with extractC_inl/extractC_inr to give the Δ^c-specific reductions.

def ConnesKreimer.cutSummandsCP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : RoseTree (α ⊕ β) → Multiset (Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β))

The Δ^c cut summands cut at non-trace subtrees, leaving trace placeholders, and skip cuts at trace leaves.

Equations

• ConnesKreimer.cutSummandsCP τ = ConnesKreimer.cutSummandsG (ConnesKreimer.extractC τ)

theorem ConnesKreimer.cutSummandsCP_def {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (T : RoseTree (α ⊕ β)) : cutSummandsCP τ T = cutSummandsG (extractC τ) T

@[simp]

theorem ConnesKreimer.cutSummandsCP_node {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : cutSummandsCP τ (RoseTree.node a cs) = Multiset.map (fun (p : Multiset (RoseTree (α ⊕ β)) × List (RoseTree (α ⊕ β))) => (p.1, RoseTree.node a p.2)) (cutListSummandsG (extractC τ) cs)

Sanity: the trace policy on leaves

Trace specialization

The Δ^c policy extractC (τ ∘ UnorderedTree.mk) is ExtractInvariant:

• For Sum.inl _-rooted inputs, extractC returns some [traceLeaf (τ (mk t))].
• For Sum.inr _-rooted inputs, extractC returns none.

Both cases are determined by the root label and the τ value, both of which are Perm-invariant.

theorem ConnesKreimer.extractC_mkComp_invariant {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) : ExtractInvariant (extractC (τ ∘ UnorderedTree.mk))

The Δ^c extract policy is ExtractInvariant.

theorem ConnesKreimer.cutSummandsCP_proj_perm {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) {t s : RoseTree (α ⊕ β)} (h : t.Perm s) : Multiset.map projSummand (cutSummandsCP (τ ∘ UnorderedTree.mk) t) = Multiset.map projSummand (cutSummandsCP (τ ∘ UnorderedTree.mk) s)

Δ^c cut-summand-projection invariance under Perm.

Descent of cutSummandsCP through UnorderedTree.mk

noncomputable def ConnesKreimer.cutSummandsCN {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) : UnorderedTree (α ⊕ β) → Multiset (Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β))

The UnorderedTree Δ^c cut summands, descended from cutSummandsCP via Quotient.lift using the descent invariance cutSummandsCP_proj_perm.

Equations

• ConnesKreimer.cutSummandsCN τ = Quotient.lift (fun (T : RoseTree (α ⊕ β)) => Multiset.map ConnesKreimer.projSummand (ConnesKreimer.cutSummandsCP (τ ∘ UnorderedTree.mk) T)) ⋯

@[simp]

theorem ConnesKreimer.cutSummandsCN_mk {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : RoseTree (α ⊕ β)) : cutSummandsCN τ (UnorderedTree.mk T) = Multiset.map projSummand (cutSummandsCP (τ ∘ UnorderedTree.mk) T)

theorem ConnesKreimer.cutSummandsCN_numEdges {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : p ∈ cutSummandsCN τ T → (Multiset.map UnorderedTree.numEdges p.1).sum + p.2.numNodes = T.numNodes

Δ^c cut summands conserve edges, since the trace marker replaces the cut subtree by a unit-weight leaf, so crown edges plus trunk weight recover the tree weight exactly. Descends cutSummandsG_numNodes through UnorderedTree.mk.

theorem ConnesKreimer.cutSummandsCN_filter_empty {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) : Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1.card = 0) (cutSummandsCN τ T) = {(0, T)}

The empty cut (0, T) is the unique cut summand of cutSummandsCN τ T with empty crown.

theorem ConnesKreimer.zero_mem_cutSummandsCN {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) : (0, T) ∈ cutSummandsCN τ T

The empty cut is a trace cut.

theorem ConnesKreimer.cutSummandsCN_mem_subtrees_of_mem_crown {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) {T : UnorderedTree (α ⊕ β)} {p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} (hp : p ∈ cutSummandsCN τ T) {x : UnorderedTree (α ⊕ β)} (hx : x ∈ p.1) : x ∈ T.subtrees

Every crown component of a Δ^c cut of T is a subtree of T.

theorem ConnesKreimer.cutSummandsCN_filter_crown_eq_singleton {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (τ : UnorderedTree (α ⊕ β) → β) {M T : UnorderedTree (α ⊕ β)} (hM : M.value.isLeft = true) (hcount : Multiset.count M T.subtrees = 1) (hTM : T ≠ M) : Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1 = {M}) (cutSummandsCN τ T) = {({M}, M.replace (UnorderedTree.leaf (Sum.inr (τ M))) T)}

A lexical subtree M occurring exactly once below the root of T is extracted by exactly one Δ^c cut, whose trunk is T with M replaced by its trace.