Docs / Syntax / Minimalist / Workspace / Merge / External

External Merge

import Linglib.Syntax.Minimalist.Workspace.Merge.External · namespace Minimalist.Merge

Source

External Merge (Lemma 1.4.1 of Marcolli, Chomsky and Berwick) is Merge of two components S, S' of a workspace. It replaces them by node lbl {S, S'} and leaves the rest unchanged. For a two-object workspace this holds over every cut enumeration admitting Merge (mergeOpG_pair), in particular at the pruning and trace cuts. With a residual workspace F̂ it holds when no component of F̂ has S or S' as a subtree (mergeOpG_pair_residual), since such a workspace passes through Merge unchanged (mergeOpG_of'_mul). The book's Merge, at the deletion cuts, reaches these through the contraction of unary vertices (mergeOp_eq_rename_contractUnary_comp), so its forms hold of objects without unary vertices, as syntactic objects are.

The proof of mergeOpG_pair expands the coproduct of {S, S'} into four cross-terms of the primitive terms and the cut sums of S and S'. Only the primitive term survives: a cut of S' alone would need crown {S'}, and cuts of both would need crowns reassembling {S, S'}, and both are ruled out by the edge bound of IsMergeCuts.

Main results

References

Declarations

L123–164

Merge commutes with a spectator workspace F none of whose components has S or S' as a subtree.

theorem mergeOpG_of'_mulL166–181
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) {S S' : UnorderedTree α} {F : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ T ∈ F, Disjoint {S, S'} T.subtrees) (w : ConnesKreimer R (UnorderedTree α)) :
(mergeOpG cuts lbl S S') (ConnesKreimer.of' F * w) = ConnesKreimer.of' F * (mergeOpG cuts lbl S S') w
L183–191

External Merge of S and S' beside a workspace F̂ none of whose components contains them leaves F̂ unchanged (Marcolli et al. 2025 Lemma 1.4.1).

theorem mergeOpG_pair_residualL193–201
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) {S S' : UnorderedTree α} {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ T ∈ Fhat, Disjoint {S, S'} T.subtrees) :
(mergeOpG cuts lbl S S') (ConnesKreimer.of' ({S, S'} + Fhat)) = ConnesKreimer.of' ({UnorderedTree.node lbl {S, S'}} + Fhat)

External Merge with a residual workspace, all of whose objects are without unary vertices.

theorem mergeOp_pair_residualL203–216
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' : UnorderedTree α} {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hS : S.numUnary = 0) (hS' : S'.numUnary = 0) (hF : ∀ T ∈ Fhat, Disjoint {S, S'} T.subtrees) (hFu : ∀ T ∈ Fhat, T.numUnary = 0) :
(mergeOp lbl S S') (ConnesKreimer.of' ({S, S'} + Fhat)) = ConnesKreimer.of' ({UnorderedTree.node lbl {S, S'}} + Fhat)

External Merge at the trace cuts

External Merge at the trace cuts with a residual workspace.

theorem mergeOpC_pair_residualL229–236
{R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (lbl : α ⊕ β) {S S' : UnorderedTree (α ⊕ β)} {Fhat : UnorderedTree.Forest (UnorderedTree (α ⊕ β))} (hF : ∀ T ∈ Fhat, Disjoint {S, S'} T.subtrees) :
(mergeOpC τ lbl S S') (ConnesKreimer.of' ({S, S'} + Fhat)) = ConnesKreimer.of' ({UnorderedTree.node lbl {S, S'}} + Fhat)