Internal Merge bridge: algebraic ↔ linguistic #
@cite{marcolli-chomsky-berwick-2025}
Realizes M-C-B Proposition 1.4.2 (book p. 50): Internal Merge as a composition of two algebraic Merges —
IM(mover, T) = mergeOp mover (T/mover) ∘ mergeOpUnit mover
where the first stage mergeOpUnit mover selects the cut on T whose
cutForest equals {mover} (yielding T/mover ⊗ 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 the cutscwithcutForest c = {β}. Under uniqueness (single such cutc0), the sum collapses.mergeOp_im_composition,mergeOp_im_composition_moverLeft: the IM composition theorem. Under unique-cut-witness hypotheses, the two-stage pipeline reduces to EM Case 1 (mergeOp_pair_residualwith empty F̂).mergeOp_im_matches_Step: bridge to linguisticStep.imvia((Step.im mover traceId).apply current).toHc. Closes the IM gap.
Status #
All theorems sorry-free as of Phase 7c (commits 0.230.766-0.230.767).
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 β (forestToHc {T}). Unfolds the
operator chain through comulTreeDel's primitive-plus-cut-sum
decomposition; each cut's contribution is filtered by mergePostUnit's
δ_{β, 1} projection, surviving only when the cut-forest equals {β}.
The primitive T ⊗ 1 term contributes forestToHc {β} if T = β,
else 0.
Unique-cut specialization of mergeOpUnit_apply_singleton. Under
the hypotheses that
T ≠ β(β is not the whole tree, so the primitive part vanishes), andc0is the unique admissible cut on T whose cut-forest is{β},
the per-cut sum collapses to a single contribution. This is the form used by the IM composition theorem: it pulls β out of T and leaves the deletion-remainder of c0 on the right channel.
Note: uniqueness is a substrate convenience, NOT a M-C-B requirement. M-C-B's Prop 1.4.2 (book p. 50) only requires "β is an accessible term of a connected component of F isomorphic to T" — it does NOT stipulate uniqueness, and multi-occurrence is genuinely allowed (yielding a sum output, structurally parallel to the EM multi-matching issue resolved for the F̂-residual case in Phase 7b-A). The unique-cut hypothesis here matches the worked example on book pp. 52–53 (which happens to have a single occurrence) but specializes the proposition. Generalizing to the sum-output case is queued.
M-C-B Proposition 1.4.2 (book p. 50): Internal Merge as composition.
The two-step composition mergeOp Q β ∘ mergeOpUnit β applied to the
singleton workspace {T} produces the merged tree .node Q β, where
Q = T/β is identified via the deletion-remainder of the unique cut
extracting β from T.
Hypotheses:
c0is the unique admissible cut on T withcutForest = {β}(the "β is uniquely positioned in T" hypothesis; multi-occurrence case defers to a sum-output formulation).c0.remainderDeletion = some Q(the cut produces a non-trivial remainder; for IM we always have at least the trace-replaced root).T ≠ β(β is a proper subtree, not the whole workspace).
Note: no β ≠ Q hypothesis is required — mergeOp_pair handles the
diagonal case Q = β correctly (the workspace becomes {β, β} and
the merged tree is .node β β).
Quotient-structure note: under comulDelAlgHom (the deletion variant
Δ^d, which mergeOp uses), the deeper copy of β is removed from T
via edge contraction — book p. 53 eq. (1.4.2) shows T₁ = T/^d T₂
with {the, apple} struck through, not replaced by a trace. Trace
replacement is the Δ^c story (book p. 53 bottom). So the algebraic
quotient Q = T/β here has β's leaves removed entirely, which makes
β ≠ Q typical but not enforced by the substrate. The Step.im
bridge (Phase 7c.4) reconciles this with the linguistic-layer
mkTrace sentinel via a trace-aware SyntacticObject.toHc
projection.
The proof is two steps:
- Apply
mergeOpUnit_apply_singleton_uniqueto reduce the innermergeOpUnit β (forestToHc {T})toforestToHc {β, Q}. - Apply EM Case 1 (
mergeOp_eps_zero_pairafter collapsing to the unweighted form viamergeOp_eps_one) to mergeQandβinto.node Q β.
Caveat (book p. 52): This composition is the algebraic realization
of IM, but mergeOpUnit (= M_{β, 1}) is NOT itself a Merge operation —
it only exists as the first half of this composition, like virtual
particles in physics.
Step.im argument-order variant of mergeOp_im_composition.
Step.im mover traceId current = .node mover (current.replace mover (mkTrace traceId))
has mover LEFT, traced (= the algebraic Q) RIGHT. M-C-B's M_{T/β, β}
has Q LEFT, β RIGHT (the convention mergeOp_im_composition follows).
This swap-variant produces forestToHc {.node β Q} instead of
{.node Q β}, matching Step.im's constructor order. The proof is
structurally simpler than the swap-needing version:
{β} + {Q} = {β, Q} definitionally (no add_comm needed).
Step.im algebraic bridge (M-C-B Prop 1.4.2 specialization).
Given the cut data c0 linking the algebraic deletion-quotient on
current.toHc to the trace-replaced linguistic quotient
(current.replace mover (mkTrace traceId)).toHc, the IM composition
mergeOp mover.toHc Q ∘ mergeOpUnit mover.toHc reproduces
((Step.im mover traceId).apply current).toHc.
Closes the IM gap in the algebraic-↔-linguistic Merge bridge, completing Phase 7c.
§4: IM cost-survival at ε = 0 (M-C-B Prop 1.5.1 bullet 3) #
@cite{marcolli-chomsky-berwick-2025} Proposition 1.5.1 says: "in the
limit ε → 0, only derivations in which all the Merge operations are
Internal Merge and External Merge remain." Sideward suppression is
proven in Sideward.lean §4.1; this section proves the IM positive
direction — IM via composition at ε = 0 produces a non-zero result
(weight 1).
Operationally, IM's cost-zero status follows from rule 4
(c(ℳ(T, 1)) = 0) for stage 1 plus rule 5 (member-depth 0) for stage 2,
with no need for rule 2's negative quotient weight ε^{-d_v} to be
separately tracked in substrate.
Caveat (MCB virtual-particles, §1.4.3). Our two-stage realization
materializes the workspace {T_v, T_i/T_v} between stages 1 and 2,
whereas MCB's signed-weight cost calculation c(ℳ(T_v, T_i/T_v)) = d_v − d_v = 0 works directly on a single ℳ action without
instantiating the intermediate workspace. The two formulations agree
numerically; the operational substitution requires accepting ℳ_{β,1}
as a (virtual) intermediate stage. See @cite{marcolli-chomsky-berwick-2025}
on the "virtual particles" caveat for the unit-stage operator.
Scope. This section directly realizes Prop 1.5.1 bullets 1+3 (cost-0
characterization + ε=0 limit) at the per-merge level. Bullet 2 ("for ε < 1,
IM/EM are leading-order terms in any derivation") follows compositionally
from bullet 3 plus non-negativity of the cost weights: each merge step's
constant (ε^0) coefficient is non-zero for EM/IM (this section + EM
analogues in External.lean) and zero for Sideward (Sideward.lean §4.1),
so a derivation chain's constant coefficient equals the product of
per-step constant coefficients — yielding the EM/IM-only contribution.
The chain-level bullet 2 statement is queued as a small follow-up
(induction over the derivation chain length).
IM cost-survival, ε = 0 (M-C-B Prop 1.5.1 bullet 3, IM positive
direction). At ε = 0, the IM composition mergeOp_eps 0 mover (T/mover) ∘ mergeOpUnit mover produces a NON-ZERO output of weight 1
(= forestToHc {.node mover (T/mover)}), confirming that IM is one
of the surviving derivations in the cost limit.
Compare with mergeOp_eps_zero_for_sideward_2b/3a/3b (in Sideward.lean
§4.1) which prove that Sideward variants vanish at ε = 0. Together
they realize MCB Prop 1.5.1's "only IM and EM survive" claim.
Structurally identical to mergeOp_im_composition_moverLeft (above)
but using mergeOp_eps 0 instead of mergeOp for stage 2. The proof
swaps mergeOp_pair for mergeOp_eps_zero_pair.
IM cost-survival, ε = 0, original (Q-LEFT) argument order. Analog
of mergeOp_im_composition. Q is the LEFT argument of the second
Merge stage; the result has Q-LEFT, β-RIGHT structure.
Step.im algebraic bridge at ε = 0 (M-C-B Prop 1.5.1, IM positive
direction, linguistic specialization). The IM composition at ε = 0
reproduces ((Step.im mover traceId).apply current).toHc with
weight 1, demonstrating that IM survives the Minimal Search cost
limit and is therefore one of the dominant Merge operations in
actual derivations.