External Merge bridge: algebraic ↔ linguistic

[MCB25]

Realizes M-C-B §1.4 Lemma 1.4.1 (External Merge) at the algebraic level on the canonical carrier ConnesKreimer R (Nonplanar α) and bridges to linguistic Step.emR/Step.emL.

Contents

Lemma 1.4.1, F̂ = ∅ subcase (mergeOp_pair). For any pair (S, S') : Nonplanar α and any root label lbl, mergeOp lbl S S' applied to of' {S, S'} yields of' {Nonplanar.node lbl {S, S'}}. Proof: expand the merge coproduct Δ^ρ({S, S'}) = comulTreeN S * comulTreeN S' (comulForestN_cons), distribute the prim/cut split of each factor, and evaluate the 4 cross-terms via mergePost_basis_tensor. Only the prim × prim cross-term survives; the other three vanish because no proper cut extracts a whole tree as its crown (cutSummandsN_crown_ne_singleton) and vertex conservation (cutSummandsN_numNodes) forbids two crowns from reassembling {S, S'}.

Lemma 1.4.1 with residual workspace F̂ (mergeOp_factor_out_singleton, mergeOp_pair_residual, MCB "Case 1"). Under CutAvoidingForestN ({S, S'}) F̂ (the cutSummandsN-based disjointness predicate of CutAvoidingNonplanar: each T ∈ F̂ differs from S, S' and no Δ^ρ cut of T extracts either as a crown), Merge factors through multiplication by the spectator components of' {T}; an induction on F̂ assembles the full Case-1 result. mergeOp_factor_out_singleton is the inductive step: mergeOp lbl S S' (of' {T} * w) = of' {T} * mergeOp lbl S S' w, isolating the surviving empty-cut summand of comulTreeN T via cutSummandsN_filter_card_zero.

The Minimalism-specific bridges (mergeOp_emR/emL_matches_Step) specialize to R = ℤ, α = LIToken ⊕ Unit. They take the head label L of the merged node and a coherence hypothesis h_coh factoring (current * item).toNonplanar as Nonplanar.node (Sum.inl L) {current.toNonplanar, item.toNonplanar} — the labeling convention fixed in Merge.Defs's planarToNonplanar (each internal node decorated with its head leaf). This is the coupling point that validates the carrier bridge's design.

Deferred (substrate gap)

• §3-4: cost-weighted Merge M^ε and the ε → 0 Sideward-elimination chain (mergeOp_eps_zero_*, em_only_chain_eps_zero). Needs an ε-weighted Δ^ρ (a cutTotalDepth analogue on cutSummandsN), not yet in the substrate. Once it lands, the EM-only chain can ride either mergeOp (unweighted) or the cost-weighted operator.

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

Algebraic Merge on a 2-tree workspace (M-C-B Lemma 1.4.1, F̂ = ∅ subcase). For any pair (S, S') : Nonplanar α and root label lbl, mergeOp lbl S S' applied to the basis vector of' {S, S'} yields of' {Nonplanar.node lbl {S, S'}}.

The merge coproduct Δ^ρ({S, S'}) = comulTreeN S * comulTreeN S' splits each factor into its full-extraction ofTree T ⊗ 1 term plus the proper-cut sum; distributing gives 4 cross-terms. Only prim × prim survives mergePost; the three sum-bearing terms vanish via cutSummandsN_crown_ne_singleton (no proper cut's crown is {S} or {S'}) and cutSummandsN_numNodes (two proper crowns under-count {S, S'}'s vertices).

theorem Minimalist.Merge.mergeOp_factor_out_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (RootedTree.Nonplanar α)] (lbl : α) {S S' T : RootedTree.Nonplanar α} (hT_S : RootedTree.ConnesKreimer.CutAvoidingN S T) (hT_S' : RootedTree.ConnesKreimer.CutAvoidingN S' T) (w : RootedTree.ConnesKreimer R (RootedTree.Nonplanar α)) : (mergeOp lbl S S') (RootedTree.ConnesKreimer.of' {T} * w) = RootedTree.ConnesKreimer.of' {T} * (mergeOp lbl S S') w

Factor-out lemma (MCB Lemma 1.4.1 Case 1, inductive step). Under CutAvoidingN S T and CutAvoidingN S' T (T ≠ S, S' and no Δ^ρ cut of T extracts S or S' as a crown), mergeOp lbl S S' commutes with left multiplication by the spectator of' {T}:

mergeOp lbl S S' (of' {T} * w) = of' {T} * mergeOp lbl S S' w.

Proof: comulAlgHomN (of' {T} * w) = comulTreeN T * comulAlgHomN w. The ofTree T ⊗ 1 term vanishes ({T} ⊄ {S, S'}); the cut-sum splits via cutSummandsN_filter_card_zero into the surviving empty cut (0, T) — which by Nonplanar-tensor commutativity and mergePost_right_one_tmul yields of' {T} * mergeOp lbl S S' w — and the nonempty cuts, each annihilated since a crown ≤ {S, S'} containing neither S nor S' must be empty.

theorem Minimalist.Merge.mergeOp_pair_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (RootedTree.Nonplanar α)] (lbl : α) {S S' : RootedTree.Nonplanar α} {Fhat : RootedTree.Forest (RootedTree.Nonplanar α)} (hF : RootedTree.ConnesKreimer.CutAvoidingForestN {S, S'} Fhat) : (mergeOp lbl S S') (RootedTree.ConnesKreimer.of' ({S, S'} + Fhat)) = RootedTree.ConnesKreimer.of' ({RootedTree.Nonplanar.node lbl {S, S'}} + Fhat)

Algebraic Merge with residual workspace (M-C-B Lemma 1.4.1, Case 1). For any pair (S, S') and residual workspace Fhat with CutAvoidingForestN ({S, S'}) Fhat (S, S' ∉ Fhat as components, no cut on any T ∈ Fhat extracts S or S' — excludes the non-primitive matchings of the full coproduct, restricting to External Merge's member-level contribution per MCB Remark 1.3.8), Merge factors the spectator workspace through:

mergeOp lbl S S' (of' ({S, S'} + Fhat)) = of' ({Nonplanar.node lbl {S, S'}} + Fhat).

Induction on Fhat via mergeOp_factor_out_singleton. Without the disjointness, mergeOp produces the full sum-over-matchings (including Sideward contributions); MCB eliminate those via Minimal-Search cost weighting in the ε → 0 limit (the deferred M^ε arc).

The linguistic External-Merge bridges mergeOp_emR/emL_matches_Step (which related mergeOp (Sum.inl L) on the head-decorated toNonplanar projection to the legacy Step.emR/emL) have been retired by the single-carrier migration. On the bare SO carrier the bridge is Workspace.lean's SO.merge_toForest (mergeOp_pair with the bare Sum.inr () label).