Internal Merge bridge: algebraic ↔ linguistic #
Realizes M-C-B Proposition 1.4.2 (book p. 50): Internal Merge as a
composition of two algebraic Merges on the canonical carrier
ConnesKreimer R (Nonplanar α) —
IM(mover, T) = mergeOp lbl mover (T/mover) ∘ mergeOpUnit mover
where the first stage mergeOpUnit mover selects the Δ^ρ cut on T whose crown
forest equals {mover} (yielding mover ⊗ (T/mover)), and the second stage
performs External Merge between mover and the deletion-quotient.
Contents #
mergeOpUnit_apply_singleton{,_unique}: per-cut decomposition of the unit-mover stagemergeOpUnit β. Surviving contributions are exactly thecutSummandsN Tsummandspwithp.1 = {β}. Under uniqueness (the filtered sub-multiset is the singleton{p0}), the sum collapses.mergeOp_im_composition,mergeOp_im_composition_moverLeft: the IM composition theorem. Under the unique-cut hypothesis, the two-stage pipeline reduces to EM Case 1 (mergeOp_pair).mergeOp_im_matches_Step: bridge to linguisticStep.imvia((Step.im mover traceId).apply current).toNonplanar.
Deferred (substrate gap) #
§4 — IM cost-survival at ε = 0 (mergeOp_eps_zero_im_*, MCB Prop 1.5.1 bullet 3)
— rides the same ε-weighted Δ^ρ gap as External's ε arc (no cutTotalDepth on
cutSummandsN). Queued behind that substrate.
Caveat (M-C-B p. 52 "virtual particles"): the mergeOpUnit stage M_{β,1} is
virtual — not a stand-alone Merge in M-C-B's formalism. It is introduced as a
bookkeeping device to factor IM as composition; the linguistic Merge is the full
IM, not the unit stage on its own.
Per-cut reduction of mergeOpUnit β (of' {T}). Unfolds the operator chain
through comulTreeN's primitive-plus-cut-sum decomposition; each cut's
contribution is filtered by mergePostUnit's δ_{β, 1} projection, surviving
only when the crown forest equals {β}.
The primitive ofTree T ⊗ 1 term contributes of' {β} if T = β, else 0.
Unique-cut specialization of mergeOpUnit_apply_singleton. When T ≠ β
(β is not the whole tree, so the primitive part vanishes) and p0 is the
unique cutSummandsN T summand with crown {β} (the filtered sub-multiset
is {p0}), the per-cut sum collapses to a single contribution of' {β} * ofTree p0.2 — pulling β out of T and leaving the deletion-remainder on the
right channel.
Uniqueness is a substrate convenience, not a M-C-B requirement. MCB Prop 1.4.2 only requires "β is an accessible term of a component isomorphic to T", allowing multi-occurrence (a sum output). The single-summand hypothesis matches the worked example (book pp. 52–53).
M-C-B Proposition 1.4.2 (book p. 50): Internal Merge as composition,
mover-LEFT order. Step.im mover traceId current = .node mover (current.replace mover (mkTrace traceId)) has mover LEFT, traced (the algebraic Q) RIGHT. The
two-step composition mergeOp lbl β Q ∘ mergeOpUnit β applied to {T} produces
of' {Nonplanar.node lbl {β, Q}}, where Q = T/β is the deletion-remainder of
the unique cut extracting β.
The label lbl of the merged root is a parameter (the operator layer is
label-generic).
IM composition, Q-LEFT (M-C-B M_{T/β, β}) order. Q is the LEFT argument of
the second merge; the result has Q-LEFT, β-RIGHT structure
of' {Nonplanar.node lbl {Q, β}}.
The linguistic Internal-Merge bridge mergeOp_im_matches_Step (which related the
mergeOp ∘ mergeOpUnit composition on the head-decorated toNonplanar projection to
the legacy Step.im + ⊕ Nat trace index) has been retired by the single-carrier
migration. On the bare SO carrier the bridge is Workspace.lean's
SO.intMerge_toForest (mergeOp_im_composition with the bare Sum.inr () label and
the index-free SO.traceLeaf).