Internal Merge

Internal Merge (Proposition 1.4.2 of Marcolli, Chomsky and Berwick) is the composition M_{T/β,β} ∘ M_{β,1}. The unit stage selects a cut of T with crown {β}, giving the two-object workspace {β, T/β}, and External Merge then merges β with the quotient. When one cut extracts β, the composition yields node lbl {T/β, β} over every cut enumeration admitting Merge (mergeOpG_im_composition). At the pruning cuts the quotient is the deletion remainder; at the trace cuts it keeps a trace in place of β (mergeOpC_im_composition).

Main results

• Minimalist.Merge.mergeOpUnitG_apply_singleton, mergeOpUnitG_apply_singleton_unique: the unit stage on one tree, a sum over the cuts with crown {β}.
• Minimalist.Merge.mergeOpUnitG_ofTree_mul, mergeOpUnitG_apply_singleton_unique_residual: the unit stage beside a spectator workspace.
• Minimalist.Merge.mergeOpG_im_composition, mergeOp_im_composition, mergeOpC_im_composition: Internal Merge as a composition of Merges.
• Minimalist.Merge.mergeOpG_im_composition_residual: Internal Merge beside a spectator workspace.

Implementation notes

The composition theorems assume a single cut extracting β, as in the book's worked example. Proposition 1.4.2 does not; with several occurrences of β the unit stage is a sum over them (mergeOpUnitG_apply_singleton).

References

• [MCB25]

theorem Minimalist.Merge.mergeOpUnitG_apply_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} (β T : UnorderedTree α) : (mergeOpUnitG cuts β) (ConnesKreimer.of' {T}) = (if T = β then ConnesKreimer.of' {β} else 0) + (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => if p.1 = {β} then ConnesKreimer.of' {β} * ConnesKreimer.ofTree p.2 else 0) (cuts T)).sum

On one tree T, the primitive term of the unit stage contributes β if T = β, and each cut with crown {β} contributes β beside its trunk.

theorem Minimalist.Merge.mergeOpUnitG_apply_singleton_unique {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} (β T : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (hTβ : T ≠ β) : (mergeOpUnitG cuts β) (ConnesKreimer.of' {T}) = ConnesKreimer.of' {β} * ConnesKreimer.ofTree p0.2

When T ≠ β and exactly one cut of T has crown {β}, the unit stage moves β to its own component beside that cut's trunk.

theorem Minimalist.Merge.mergeOpUnitG_ofTree_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] {β T : UnorderedTree α} (hT : β ∉ T.subtrees) (w : ConnesKreimer R (UnorderedTree α)) : (mergeOpUnitG cuts β) (ConnesKreimer.ofTree T * w) = ConnesKreimer.ofTree T * (mergeOpUnitG cuts β) w

The unit stage commutes with a spectator component T that does not have β as a subtree.

theorem Minimalist.Merge.mergeOpUnitG_apply_singleton_unique_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (β T : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (hTβ : T ≠ β) {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ U ∈ Fhat, β ∉ U.subtrees) : (mergeOpUnitG cuts β) (ConnesKreimer.of' ({T} + Fhat)) = ConnesKreimer.of' ({β, p0.2} + Fhat)

With a residual workspace F̂ none of whose components has β as a subtree, the unit stage on {T} + F̂ splits β off T and leaves F̂ unchanged.

theorem Minimalist.Merge.mergeOpG_im_composition {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) : (mergeOpG cuts lbl Q β) ((mergeOpUnitG cuts β) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, β}}

Internal Merge as the composition M_{T/β,β} ∘ M_{β,1} over a cut enumeration admitting Merge, for β extracted from T by a single cut with trunk Q.

theorem Minimalist.Merge.mergeOpG_im_composition_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ U ∈ Fhat, Disjoint {Q, β} U.subtrees) : (mergeOpG cuts lbl Q β) ((mergeOpUnitG cuts β) (ConnesKreimer.of' ({T} + Fhat))) = ConnesKreimer.of' ({UnorderedTree.node lbl {Q, β}} + Fhat)

Internal Merge with a residual workspace F̂, none of whose components has β or the trunk Q as a subtree.

theorem Minimalist.Merge.mergeOp_im_composition {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (ConnesKreimer.cutSummandsN T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) : (mergeOp lbl Q β) ((mergeOpUnit β) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, β}}

Internal Merge at the pruning cuts.

theorem Minimalist.Merge.mergeOpC_im_composition {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (lbl : α ⊕ β) (m T Q : UnorderedTree (α ⊕ β)) (p0 : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1 = {m}) (ConnesKreimer.cutSummandsCN τ T) = {p0}) (h_remainder : p0.2 = Q) (hTm : T ≠ m) : (mergeOpC τ lbl Q m) ((mergeOpUnitC τ m) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, m}}

At the trace cuts Internal Merge merges the mover m with the trunk Q, which keeps a trace in its place.