Merge on the syntactic-object carrier

Merge on the carrier is the bare binary node SyntacticObject.merge with root label Sum.inr none. This file identifies it with the algebraic Merge operator of Merge/Basic.lean on workspaces lifted along of': External Merge of two objects is mergeOp_pair, and Internal Merge of a mover with its remainder is the two-stage composition mergeOp_im_composition, given the unique Δ^ρ cut extracting the mover.

Main results

• Minimalist.SyntacticObject.mergeOp_node: External Merge on the carrier is mergeOp.
• Minimalist.SyntacticObject.mergeOp_node_im: Internal Merge on the carrier is mergeOp ∘ mergeOpUnit.

References

• [marcolli-chomsky-berwick-2025], §1.4 (Lemma 1.4.1, Proposition 1.4.2)

theorem Minimalist.SyntacticObject.mergeOp_node (S S' : SyntacticObject) : (Merge.mergeOp (Sum.inr none) ↑S ↑S') (ConnesKreimer.of' {↑S, ↑S'}) = ConnesKreimer.of' {↑(S.merge S')}

External Merge on the carrier is the algebraic Merge with the bare root label on the two-object workspace.

theorem Minimalist.SyntacticObject.mergeOp_merge_im (mover remainder T : SyntacticObject) (p0 : UnorderedTree.Forest (UnorderedTree Vertex) × UnorderedTree Vertex) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree Vertex) × UnorderedTree Vertex) => p.1 = {↑mover}) (ConnesKreimer.cutSummandsN ↑T) = {p0}) (h_remainder : p0.2 = ↑remainder) (hT : ↑T ≠ ↑mover) : (Merge.mergeOp (Sum.inr none) ↑remainder ↑mover) ((Merge.mergeOpUnit ↑mover) (ConnesKreimer.of' {↑T})) = ConnesKreimer.of' {↑(remainder.merge mover)}

Internal Merge on the carrier is the two-stage algebraic Merge, given the unique Δ^ρ cut p0 of T extracting mover with remainder remainder.