Documentation

Linglib.Syntax.Minimalist.Merge.External

External Merge #

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 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 #

source
instance Minimalist.Merge.instIsMergeCutsCutSummandsN {α : Type u_2} :
IsMergeCuts ConnesKreimer.cutSummandsN
source
instance Minimalist.Merge.instIsMergeCutsSumCutSummandsCN {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) :
IsMergeCuts (ConnesKreimer.cutSummandsCN τ)
source
theorem Minimalist.Merge.mergeOpG_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) (S S' : UnorderedTree α) :
(mergeOpG cuts lbl S S') (ConnesKreimer.of' {S, S'}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}}

External Merge of a two-object workspace, over a cut enumeration admitting Merge.

source
theorem Minimalist.Merge.mergeOp_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) (S S' : UnorderedTree α) :
(mergeOp lbl S S') (ConnesKreimer.of' {S, S'}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}}

External Merge of a two-object workspace at the pruning cuts.

source
theorem Minimalist.Merge.mergeOpG_ofTree_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) {S S' T : UnorderedTree α} (hT_S : S ∉ T.subtrees) (hT_S' : S' ∉ T.subtrees) (w : ConnesKreimer R (UnorderedTree α)) :
(mergeOpG cuts lbl S S') (ConnesKreimer.ofTree T * w) = ConnesKreimer.ofTree T * (mergeOpG cuts lbl S S') w

Merge commutes with a spectator component T that has neither S nor S' as a subtree ([MCB25] Lemma 1.4.1). The primitive term of T does not fit inside {S, S'}, no nonempty cut of T extracts S or S', and the empty cut passes T through to the right channel.

source
theorem Minimalist.Merge.mergeOpG_of'_mul {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

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

source
theorem Minimalist.Merge.mergeOp_ofTree_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' T : UnorderedTree α} (hT_S : S ∉ T.subtrees) (hT_S' : S' ∉ T.subtrees) (w : ConnesKreimer R (UnorderedTree α)) :
(mergeOp lbl S S') (ConnesKreimer.ofTree T * w) = ConnesKreimer.ofTree T * (mergeOp lbl S S') w

Merge at the pruning cuts commutes with a spectator component that has neither S nor S' as a subtree.

source
theorem Minimalist.Merge.mergeOpG_pair_residual {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 F̂ none of whose components has S or S' as a subtree ([MCB25] Lemma 1.4.1). Without the hypothesis Merge also matches accessible terms inside F̂, the Sideward cases of Merge/Sideward.lean.

source
theorem Minimalist.Merge.mergeOp_pair_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' : UnorderedTree α} {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ T ∈ Fhat, Disjoint {S, S'} T.subtrees) :
(mergeOp lbl S S') (ConnesKreimer.of' ({S, S'} + Fhat)) = ConnesKreimer.of' ({UnorderedTree.node lbl {S, S'}} + Fhat)

External Merge at the pruning cuts with a residual workspace.

External Merge at the trace cuts #

source
theorem Minimalist.Merge.mergeOpC_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) :
(mergeOpC τ lbl S S') (ConnesKreimer.of' {S, S'}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}}

External Merge of a two-object workspace at the trace cuts.

source
theorem Minimalist.Merge.mergeOpC_pair_residual {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)

External Merge at the trace cuts with a residual workspace.