External Merge bridge: algebraic ↔ linguistic

@cite{marcolli-chomsky-berwick-2025}

Realizes M-C-B §1.4 Lemma 1.4.1 (External Merge) at the algebraic level and bridges to linguistic Step.emR/Step.emL.

Contents

§1: Lemma 1.4.1, F̂ = ∅ subcase (lines ≈ mergeOp_pair). For any pair (S, S') : TraceTree α Unit, mergeOp S S' applied to forestToHc {S, S'} yields forestToHc {.node S S'}. Proof: expand Δ^d({S, S'}) = Δ^d(S) · Δ^d(S') via comulDelAlgHom_pair, then evaluate the 4 cross-categories via mergePost_basis_tensor. Only the prim × prim cross-term survives.

The Minimalism-specific bridges (mergeOp_emR/L_matches_Step) specialize to R = ℤ, α = LIToken, with rfl bridging (.node current item).toHc = .node current.toHc item.toHc.

§2: Full Lemma 1.4.1 with residual workspace F̂ (lines ≈ mergeOp_factor_out_singleton, mergeOp_pair_residual). Under CutAvoidingForest ({S, S'}) Fhat (Connes-Kreimer "Case 1" condition, defined in Core/Combinatorics/RootedTree/CutAvoiding.lean), Merge factors through multiplication by spectator components; induction on F̂ assembles the full Case-1 result.

§3: Phase 7d limit theorem (cost-based Sideward elimination) (lines ≈ mergeOp_eps_zero_*). At ε = 0, mergeOp_eps evaluates the EM Case-1 contribution without the cut disjointness clauses — these are derived from cost minimization (Sideward weights ε^d → 0 as ε → 0). Implements M-C-B §1.5.3 + Prop 1.5.1.

Status

All theorems sorry-free as of 0.230.804.

theorem Minimalist.Merge.mergeOp_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : (mergeOp S S') (ConnesKreimer.forestToHc {S, S'}) = ConnesKreimer.forestToHc {S.node S'}

Algebraic Merge on a 2-tree workspace (M-C-B Lemma 1.4.1, Fhat = ∅ subcase, p. 49). For any pair (S, S') : TraceTree α Unit, mergeOp S S' applied to the basis vector forestToHc {S, S'} yields forestToHc {.node S S'}.

The 4 cross-term reductions are inlined as have blocks below (each consumed exactly once); the substrate-level structural lemmas cutForest_ne_singleton_self and cutForest_add_ne_insert_pair do the load-bearing elimination work.

theorem Minimalist.Merge.mergeOp_emR_matches_Step (current item : SyntacticObject) (h_coh : (current * item).toHc = current.toHc.node item.toHc) : (mergeOp current.toHc item.toHc) (ConnesKreimer.forestToHc {current.toHc, item.toHc}) = ConnesKreimer.forestToHc {((Step.emR item).apply current).toHc}

External Merge bridge (right-complement) (M-C-B Lemma 1.4.1, p. 49, Fhat = ∅ subcase). mergeOp current.toHc item.toHc applied to the 2-tree workspace {current.toHc, item.toHc} yields the singleton workspace of .node current item = (Step.emR item).apply current.

The hypothesis h_coh : (current * item).toHc = .node current.toHc item.toHc is the externalize-respect property at the merged node: the Quot.out-based toHc on (current * item) happens to factor as .node current.toHc item.toHc. Per MCB §1.12.3 (book p. 116), this is the local-coherence condition that some sections satisfy at specific nodes; consumers supply the hypothesis when the section is built to respect this merge.

theorem Minimalist.Merge.mergeOp_emL_matches_Step (item current : SyntacticObject) (h_coh : (item * current).toHc = item.toHc.node current.toHc) : (mergeOp item.toHc current.toHc) (ConnesKreimer.forestToHc {item.toHc, current.toHc}) = ConnesKreimer.forestToHc {((Step.emL item).apply current).toHc}

External Merge bridge (left-specifier) (M-C-B Lemma 1.4.1, p. 49, Fhat = ∅ subcase, symmetric pair). mergeOp item.toHc current.toHc applied to {item.toHc, current.toHc} yields .node item current.

theorem Minimalist.Merge.mergeOp_factor_out_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] {S S' T : ConnesKreimer.TraceTree α Unit} (hT_S : ConnesKreimer.CutAvoiding S T) (hT_S' : ConnesKreimer.CutAvoiding S' T) (w : ConnesKreimer.Hc R α) : (mergeOp S S') (ConnesKreimer.forestToHc {T} * w) = ConnesKreimer.forestToHc {T} * (mergeOp S S') w

Factor-out lemma: under disjointness on T (T ≠ S, T ≠ S', and no cut on T extracts S or S'), mergeOp S S' commutes with multiplication by forestToHc {T} on the workspace:

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

Proof: expand comulDelAlgHom (forestToHc {T} * w) = comulTreeDel T * comulDelAlgHom w. Decompose comulTreeDel T into prim + cut sum. The prim term and non-empty cuts vanish under disjointness via mergePost_left_mul_eq_zero_of_not_le. The empty cut contributes (1 ⊗ forestToHc {T}) * comulDelAlgHom w, which by Hc-commutativity and mergePost_right_one_tmul evaluates to forestToHc {T} * mergeOp S S' w.

theorem Minimalist.Merge.mergeOp_pair_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] {S S' : ConnesKreimer.TraceTree α Unit} {Fhat : ConnesKreimer.TraceForest α Unit} (hF : ConnesKreimer.CutAvoidingForest {S, S'} Fhat) : (mergeOp S S') (ConnesKreimer.forestToHc ({S, S'} + Fhat)) = ConnesKreimer.forestToHc ({S.node S'} + Fhat)

Algebraic Merge with residual workspace (M-C-B Lemma 1.4.1, p. 49 — formalization restricted to Case 1 of §1.4.1, p. 48). For any pair (S, S') : TraceTree α Unit and any residual workspace Fhat : TraceForest α Unit such that CutAvoidingForest ({S, S'}) Fhat (S, S' ∉ Fhat as components, no cut on any T ∈ Fhat extracts S or S' — excludes secondary member-level matchings per eq. (1.3.3) and the accessible-terms-inside Sideward cases 2(b), 3(a), 3(b) per Lemmas 1.4.4 (p. 54) and 1.4.5 (p. 55)), we have

mergeOp S S' (forestToHc ({S, S'} + Fhat)) = forestToHc ({.node S S'} + Fhat).

Why these exact conditions. M-C-B Remark 1.3.8 (p. 47) clarifies that External Merge picks out the primitive part of the coproduct (member-level matchings only); the cut conditions enforce this restriction at the formalization layer by excluding the non-primitive contributions that would otherwise survive δ_{S,S'}.

Pre-Minimal-Search shortcut. This is the conditional EM result. Without the disjointness, mergeOp produces the sum-over-matchings of eq. (1.3.11), p. 45 — including Sideward contributions. M-C-B's own elimination of Sideward (per §1.5, pp. 56-59) is via Minimal Search cost weighting in the ε → 0 limit, realized in mergeOp_eps_zero_residual (below) which derives Case-1 dominance from cost minimization without the CutAvoidingForest hypothesis. The connection between the two formulations is mergeOp_eq_mergeOp_eps_zero_under_avoiding: under CutAvoidingForest both operators agree pointwise.

theorem Minimalist.Merge.mergeOp_eps_zero_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : (mergeOp_eps 0 S S') (ConnesKreimer.forestToHc {S, S'}) = ConnesKreimer.forestToHc {S.node S'}

Limit theorem (F̂ = ∅ case): at ε = 0, the cost-weighted Merge operator on the 2-tree workspace {S, S'} produces exactly forestToHc {.node S S'} — Case 1 only. The proof expands the weighted coproduct (which at ε = 0 reduces to the primitive part (T ⊗ 1) + (1 ⊗ T) per comulTreeDel_eps_zero) and shows only the prim_S × prim_S' cross-term contributes via mergePost_basis_tensor.

theorem Minimalist.Merge.mergeOp_eps_zero_factor_out_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] {S S' T : ConnesKreimer.TraceTree α Unit} (hT_ne_S : T ≠ S) (hT_ne_S' : T ≠ S') (w : ConnesKreimer.Hc R α) : (mergeOp_eps 0 S S') (ConnesKreimer.forestToHc {T} * w) = ConnesKreimer.forestToHc {T} * (mergeOp_eps 0 S S') w

Factor-out for mergeOp_eps 0: at ε = 0, mergeOp factors through forestToHc {T} multiplication for any T ≠ S, S' — without requiring the no_cut_* clauses on T (which were needed for the unweighted mergeOp_factor_out_singleton). The cut conditions are derived from cost minimization here: at ε = 0, all cuts vanish from comulTreeDel_eps 0 T, leaving only the primitive part (T ⊗ 1) + (1 ⊗ T).

theorem Minimalist.Merge.mergeOp_eps_zero_residual {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] {S S' : ConnesKreimer.TraceTree α Unit} {Fhat : ConnesKreimer.TraceForest α Unit} (hS : S ∉ Fhat) (hS' : S' ∉ Fhat) : (mergeOp_eps 0 S S') (ConnesKreimer.forestToHc ({S, S'} + Fhat)) = ConnesKreimer.forestToHc ({S.node S'} + Fhat)

Cost-derived EM Case 1 with arbitrary residual F̂. At ε = 0, the cost-weighted Merge operator on workspace {S, S'} + F̂ produces forestToHc ({.node S S'} + F̂) under just the no-duplicate-component hypothesis (S, S' ∉ F̂) — the no_cut_* clauses of CutAvoidingForest are derived from cost minimization (Sideward weights ε^d → 0).

theorem Minimalist.Merge.mergeOp_eq_mergeOp_eps_zero_under_avoiding {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] {S S' : ConnesKreimer.TraceTree α Unit} {Fhat : ConnesKreimer.TraceForest α Unit} (hF : ConnesKreimer.CutAvoidingForest {S, S'} Fhat) : (mergeOp S S') (ConnesKreimer.forestToHc ({S, S'} + Fhat)) = (mergeOp_eps 0 S S') (ConnesKreimer.forestToHc ({S, S'} + Fhat))

Connection corollary (MCB §1.5.3, EM Case 1). Under the CutAvoidingForest hypothesis, both the unweighted mergeOp (proven via mergeOp_pair_residual with the full Case 1 disjointness) and the cost-weighted mergeOp_eps 0 (proven via mergeOp_eps_zero_residual with only member disjointness, the rest derived from cost minimization) produce the same output forestToHc ({.node S S'} + Fhat).

The two formulations answer different questions:

• mergeOp_pair_residual: under Case-1 disjointness, what does the unweighted Merge produce? Answer: only EM's contribution survives because no Sideward matchings exist.
• mergeOp_eps_zero_residual: under member disjointness alone, what does the cost-weighted Merge produce at ε = 0? Answer: only EM's contribution survives because Sideward matchings exist but vanish at ε = 0.

This corollary witnesses that the two answers coincide on the EM Case-1 input, even though they reach the conclusion via different suppression mechanisms.

theorem Minimalist.Merge.mergeOp_eps_zero_emR_matches_Step (current item : SyntacticObject) (h_coh : (current * item).toHc = current.toHc.node item.toHc) : (mergeOp_eps 0 current.toHc item.toHc) (ConnesKreimer.forestToHc {current.toHc, item.toHc}) = ConnesKreimer.forestToHc {((Step.emR item).apply current).toHc}

EM cost-survival, ε = 0, right-complement (MCB Prop 1.5.1 EM positive direction, Step.emR specialization). At ε = 0, the cost-weighted Merge mergeOp_eps 0 current.toHc item.toHc applied to the workspace {current.toHc, item.toHc} produces the singleton workspace of (Step.emR item).apply current with weight 1. The EM analogue of Internal.mergeOp_eps_zero_im_matches_Step; together they realize MCB Prop 1.5.1's "EM and IM survive at ε = 0" claim at the linguistic Step bridge level.

theorem Minimalist.Merge.mergeOp_eps_zero_emL_matches_Step (item current : SyntacticObject) (h_coh : (item * current).toHc = item.toHc.node current.toHc) : (mergeOp_eps 0 item.toHc current.toHc) (ConnesKreimer.forestToHc {item.toHc, current.toHc}) = ConnesKreimer.forestToHc {((Step.emL item).apply current).toHc}

EM cost-survival, ε = 0, left-specifier (MCB Prop 1.5.1 EM positive direction, Step.emL specialization). Symmetric pair to mergeOp_eps_zero_emR_matches_Step.

§4: MCB Prop 1.5.1 chain-level (EM-only)

@cite{marcolli-chomsky-berwick-2025} §1.5 rule 5 (book p. 59) defines a derivation φ as a sequence of Merge operations and the total cost as the sum of step costs. Bullet 2 + 3 of Prop 1.5.1 (book p. 60-61) operate at the chain level: chains containing any Sideward step have weight ε^{c(φ)} → 0 in the limit ε → 0.

Linglib's Derivation (in Theories/Syntax/Minimalist/Derivation.lean) has constructors Step.emR, Step.emL, Step.im. There is no Step.sideward because Sideward is suppressed by Prop 1.5.1; there is no Step.wlm because Wholesale Late Merger derivations were never attested in Phenomena consumers and MCB §1.7 predicts wlm-outputs are derivable from EM/IM regardless.

This section provides the EM-only chain bridge: a joint linguistic+ algebraic fold that tracks the (SyntacticObject, Hc workspace) pair through each step. For EM-only chains, the algebraic ε = 0 second component matches forestToHc {current SO}.toHc at every stage. The IM chain extension requires either adding cut-data annotations to Step.im or proving cut-existence from SyntacticObject.replace semantics — deferred.

noncomputable def Minimalist.Merge.stepApplyEM_eps_zero : Step → SyntacticObject → ConnesKreimer.Hc ℤ LIToken

Single EM step at the algebraic ε = 0 level: applies mergeOp_eps 0 to the workspace {current.toHc, item.toHc} (or symmetric for emL), where item is being injected from the lexicon into the workspace. Returns the singleton workspace of the merged result.

noncomputable because it depends on mergeOp_eps. Returns 0 for IM steps (not handled at this chain level — see chain-theorem docstring for caveats).

Equations

• Minimalist.Merge.stepApplyEM_eps_zero (Minimalist.Step.emR item) x✝ = (Minimalist.Merge.mergeOp_eps 0 x✝.toHc item.toHc) (ConnesKreimer.forestToHc {x✝.toHc, item.toHc})
• Minimalist.Merge.stepApplyEM_eps_zero (Minimalist.Step.emL item) x✝ = (Minimalist.Merge.mergeOp_eps 0 item.toHc x✝.toHc) (ConnesKreimer.forestToHc {item.toHc, x✝.toHc})
• Minimalist.Merge.stepApplyEM_eps_zero x✝¹ x✝ = 0

def Minimalist.Merge.stepCoherence (step : Step) (current : SyntacticObject) : Prop

The per-step externalize-respect coherence requirement, packaged as a Prop-valued helper for chain-level consumers. For .emR/.emL, the relevant (_ * _).toHc = .node _ _ factorization; for .im, vacuous.

Equations

• Minimalist.Merge.stepCoherence (Minimalist.Step.emR item) current = ((current * item).toHc = current.toHc.node item.toHc)
• Minimalist.Merge.stepCoherence (Minimalist.Step.emL item) current = ((item * current).toHc = item.toHc.node current.toHc)
• Minimalist.Merge.stepCoherence step current = True

theorem Minimalist.Merge.stepApplyEM_eps_zero_match (step : Step) (current : SyntacticObject) (h_em : ∀ (mover : SyntacticObject) (traceId : ℕ), step ≠ Step.im mover traceId) (h_coh : stepCoherence step current) : stepApplyEM_eps_zero step current = ConnesKreimer.forestToHc {(step.apply current).toHc}

For an EM step (emR or emL), the algebraic ε = 0 application produces the singleton workspace of step.apply current. Per-step witness for the chain theorem; assembles mergeOp_eps_zero_emR/emL_matches_Step.

theorem Minimalist.Merge.em_only_chain_eps_zero (steps : List Step) (initial : SyntacticObject) (h_em_only : ∀ s ∈ steps, ∀ (mover : SyntacticObject) (traceId : ℕ), s ≠ Step.im mover traceId) (h_coh_chain : ∀ s ∈ steps, ∀ (current : SyntacticObject), stepCoherence s current) : List.foldl (fun (state : SyntacticObject × ConnesKreimer.Hc ℤ LIToken) (step : Step) => (step.apply state.1, stepApplyEM_eps_zero step state.1)) (initial, ConnesKreimer.forestToHc {initial.toHc}) steps = (List.foldl (fun (so : SyntacticObject) (step : Step) => step.apply so) initial steps, ConnesKreimer.forestToHc {(List.foldl (fun (so : SyntacticObject) (step : Step) => step.apply so) initial steps).toHc})

MCB Prop 1.5.1 chain-level, EM-only derivations (book §1.5 rule 5, p. 59). For an EM-only Step list applied to an initial SyntacticObject, the joint (linguistic SO, algebraic ε = 0 workspace) fold preserves the invariant that the workspace equals forestToHc {(current SO).toHc} at every stage. The fold's final result therefore equals (d.final, forestToHc {d.final.toHc}).

This realizes the chain-level reading of Prop 1.5.1's bullet 2 + 3 for the EM-only case: every step survives at ε = 0 with weight 1, so the entire chain produces the linguistic output's singleton workspace in Hc ℤ LIToken.

For mixed EM/IM derivations, the IM-step bridge requires cut-data annotations (queued separately).