Merge Operator on the Bialgebra of Decorated Forests

@cite{marcolli-chomsky-berwick-2025}

Per M-C-B 2025 §1.3 (Definitions 1.3.1, 1.3.2, 1.3.4), the linguistic Merge operator M_{S,S'} for a pair (S, S') : TraceTree α Unit of accessible terms is the composition

M_{S,S'} = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ^d

where:

• Δ^d is the deletion coproduct (comulDelAlgHom, M-C-B Def 1.2.8 with ω = d)
• δ_{S,S'} is the matching operator that selects coproduct terms whose left channel equals the 2-element forest {S, S'} (M-C-B Def 1.3.1)
• B ⊗ id applies grafting on the left channel: replaces the 2-element forest {S, S'} with the binary tree .node S S'
• ⊔ is the multiplication on Hc R α (forest disjoint union, the algebra structure of Hc)

This file builds the building blocks (gammaMatch, deltaMatch, graftBinary) and assembles mergeOp. The bridges to linguistic Step.apply live in Merge.External (EM) and Merge.Internal (IM).

§1: γ_{S,S'} matching projection (M-C-B Def 1.3.1)

For a fixed pair (S, S') : TraceTree α Unit, gammaMatch S S' is the linear endomorphism of Hc R α that projects onto the basis element single {S, S'} 1:

gammaMatch S S' (single F r) = if F = {S, S'} then single F r else 0

Built as Finsupp.lsingle ∘ Finsupp.lapply on the matching forest.

noncomputable def Minimalist.Merge.gammaMatch {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The matching projection γ_{S,S'} (M-C-B Def 1.3.1): keeps the coefficient of the {S, S'} basis element, sends everything else to zero.

Equations

• Minimalist.Merge.gammaMatch S S' = Finsupp.lsingle {S, S'} ∘ₗ Finsupp.lapply {S, S'}

theorem Minimalist.Merge.gammaMatch_apply_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) : (gammaMatch S S') (ConnesKreimer.forestToHc F) = if F = {S, S'} then ConnesKreimer.forestToHc F else 0

γ_{S,S'} acts as a basis-vector projection: on the basis element forestToHc F, it returns forestToHc F if F = {S, S'} and 0 otherwise. M-C-B Def 1.3.1.

§2: δ_{S,S'} matching on the left tensor channel (M-C-B Def 1.3.1)

deltaMatch S S' = gammaMatch S S' ⊗ id lifts the matching projection to act on the left channel of Hc R α ⊗ Hc R α.

noncomputable def Minimalist.Merge.deltaMatch {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α) →ₗ[R] TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)

The matching operator δ_{S,S'} on tensored coproduct output: applies gammaMatch S S' to the left channel and identity to the right.

Equations

• Minimalist.Merge.deltaMatch S S' = TensorProduct.map (Minimalist.Merge.gammaMatch S S') LinearMap.id

§3: B grafting for binary Merge (M-C-B Def 1.3.2 + Lemma 1.3.3)

graftBinaryAt S S' replaces the 2-element forest {S, S'} (basis element of Hc R α) with the binary tree .node S S' (also a basis element). All other basis elements map to zero — we only need this specialized form because the Merge action's preceding δ_{S,S'} step restricts the left channel to multiples of {S, S'} anyway.

noncomputable def Minimalist.Merge.graftBinaryAt {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The grafting operator B specialized at the pair (S, S'): maps the basis element {S, S'} to .node S S', all other basis elements to zero. M-C-B Lemma 1.3.3 for binary Merge.

Equations

• Minimalist.Merge.graftBinaryAt S S' = Finsupp.lsingle {S.node S'} ∘ₗ Finsupp.lapply {S, S'}

theorem Minimalist.Merge.graftBinaryAt_apply_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) : (graftBinaryAt S S') (ConnesKreimer.forestToHc F) = if F = {S, S'} then ConnesKreimer.forestToHc {S.node S'} else 0

B grafts on basis vectors: on forestToHc F, returns forestToHc {.node S S'} if F = {S, S'}, and 0 otherwise. Same shape as gammaMatch_apply_singleton with a different target.

§4: Merge operator (M-C-B Def 1.3.4)

mergeOp S S' = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ^d

The chain:

1. Δ^d extracts admissible cuts (deletion-with-rebinarization remainder)
2. δ_{S,S'} filters to terms where the cut forest equals {S, S'}
3. (B ⊗ id) grafts {S, S'} into .node S S' on the left channel
4. ⊔ multiplies the two channels back into a single workspace

When no admissible cut produces {S, S'} as its cut forest, all terms are killed by δ_{S,S'} and mergeOp S S' F = 0 (the empty workspace in Hc's sense).

noncomputable def Minimalist.Merge.hcMulLin {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α) →ₗ[R] ConnesKreimer.Hc R α

Multiplication on Hc R α lifted to a linear map Hc R α ⊗[R] Hc R α →ₗ[R] Hc R α. Wraps mathlib's Algebra.TensorProduct.lmul', which gives the multiplication algebra-hom for any commutative R-algebra.

Equations

• Minimalist.Merge.hcMulLin = (Algebra.TensorProduct.lmul' R).toLinearMap

noncomputable def Minimalist.Merge.mergePost {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α) →ₗ[R] ConnesKreimer.Hc R α

Post-coproduct chain ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} as a single named linear map. mergeOp factors as mergePost S S' ∘ comulDelAlgHom.toLinearMap.

Extracting this composition lets the basis-tensor and vanishing lemmas state their LHS without re-spelling the chain, and gives Phase 7c's mergeOpUnit (and any future M_{S, 1} / sideward variants) a parallel slot to define their own post-coproduct chains.

Equations

• Minimalist.Merge.mergePost S S' = Minimalist.Merge.hcMulLin ∘ₗ TensorProduct.map (Minimalist.Merge.graftBinaryAt S S') LinearMap.id ∘ₗ Minimalist.Merge.deltaMatch S S'

noncomputable def Minimalist.Merge.mergeOp {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The Merge operator M_{S,S'} per M-C-B Def 1.3.4. Factors as mergePost S S' ∘ comulDelAlgHom.

Equations

• Minimalist.Merge.mergeOp S S' = Minimalist.Merge.mergePost S S' ∘ₗ ConnesKreimer.comulDelAlgHom.toLinearMap

noncomputable def Minimalist.Merge.mergeOp_eps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) (S S' : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The cost-weighted Merge operator M^ε_{S, S'} per M-C-B eq. (1.5.1), §1.5.3 (p. 60). Factors as mergePost S S' ∘ comulDelAlgHom_eps ε. Each coproduct contribution gets weighted by ε^{cutTotalDepth c} per cut.

At ε = 1: collapses to mergeOp (unweighted). At ε = 0: only Case 1 (members-only matching) survives — Sideward contributions all carry positive cost and vanish.

The ε → 0 limit theorem mergeOp_eps_zero_residual (in Merge.External) recovers mergeOp_pair_residual WITHOUT requiring the CutAvoidingForest hypothesis: cost minimization automatically excludes Sideward Merge.

Equations

• Minimalist.Merge.mergeOp_eps ε S S' = Minimalist.Merge.mergePost S S' ∘ₗ (ConnesKreimer.comulDelAlgHom_eps ε).toLinearMap

theorem Minimalist.Merge.mergeOp_eps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) : mergeOp_eps 1 S S' = mergeOp S S'

At ε = 1, the weighted Merge operator collapses to the unweighted one.

§5: Post-coproduct chain on basis tensors

mergePost S S' evaluated on an elementary tensor forestToHc F ⊗ r is:

• forestToHc {.node S S'} * r if F = {S, S'}
• 0 otherwise

This is the load-bearing fact for proving that algebraic Merge agrees with linguistic Step.apply: every basis-tensor term in the expansion of Δ^d({S, S'}) either matches the merge target (only the primitive {S, S'} ⊗ 1 term) or is annihilated by δ_{S,S'}.

theorem Minimalist.Merge.mergePost_basis_tensor {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) (r : ConnesKreimer.Hc R α) : (mergePost S S') (ConnesKreimer.forestToHc F ⊗ₜ[R] r) = if F = {S, S'} then ConnesKreimer.forestToHc {S.node S'} * r else 0

The post-coproduct chain mergePost S S' evaluated on a basis tensor forestToHc F ⊗ r.

theorem Minimalist.Merge.gammaMatch_mul_eq_zero_of_not_le {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) (hF : ¬F ≤ {S, S'}) (a : ConnesKreimer.Hc R α) : (gammaMatch S S') (ConnesKreimer.forestToHc F * a) = 0

General γ_{S,S'}-vanishing on a left-multiplied forest: if F is NOT a sub-multiset of {S, S'}, then γ_{S,S'}(forestToHc F * a) = 0 for any a.

The hypothesis ¬ F ≤ ({S, S'} : TraceForest α Unit) says F cannot embed into {S, S'} as a sub-multiset, equivalently (by Multiset.le_iff_exists_add) F is not a left-divisor of {S, S'} in the multiset additive semigroup.

theorem Minimalist.Merge.gammaMatch_singleton_mul_eq_zero {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') (a : ConnesKreimer.Hc R α) : (gammaMatch S S') (ConnesKreimer.forestToHc {T} * a) = 0

Disjoint-singleton vanishing of γ_{S,S'} (corollary): if T ≠ S and T ≠ S', then γ_{S,S'}(forestToHc {T} * a) = 0.

theorem Minimalist.Merge.mergePost_left_mul_eq_zero_of_not_le {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) (b : ConnesKreimer.Hc R α) (hF : ¬F ≤ {S, S'}) (z : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)) : (mergePost S S') (ConnesKreimer.forestToHc F ⊗ₜ[R] b * z) = 0

Vanishing of mergePost on left-multiplied disjoint factors: if F is NOT a sub-multiset of {S, S'} and b : Hc R α is arbitrary, then for any z : Hc R α ⊗[R] Hc R α:

mergePost ((forestToHc F ⊗ b) * z) = 0.

Used to eliminate cross-terms in the F̂-residual generalization of mergeOp_pair: any term in comulTreeDel T * comulDelAlgHom w whose LEFT contribution is a forest F that doesn't fit inside {S, S'} (e.g., prim_T with F = {T} when T ≠ S, S', or non-empty cuts of T under disjointness) vanishes after mergePost.

theorem Minimalist.Merge.mergePost_right_one_tmul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (z : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)) (y : ConnesKreimer.Hc R α) : (mergePost S S') (z * 1 ⊗ₜ[R] y) = (mergePost S S') z * y

Right-multiplicativity of the post-coproduct chain by a "pure right-channel" factor 1 ⊗ y. For any z : Hc R α ⊗[R] Hc R α and any y : Hc R α:

mergePost (z * (1 ⊗ y)) = mergePost(z) * y.

Load-bearing for the F̂-residual generalization of mergeOp_pair (M-C-B Lemma 1.4.1 in full): the all-empty-cut term of comulForestDel F̂ has the form 1 ⊗ forestToHc F̂, so this lemma propagates the residual workspace F̂ through the post-coproduct chain unchanged.

§6: M_{β, 1} substrate (single-element matching, no grafting)

Per @cite{marcolli-chomsky-berwick-2025} §1.4.3.1 (book p. 50), the operator M_{β, 1} is the "first half" of Internal Merge per Prop 1.4.2:

IM = M_{T/β, β} ∘ M_{β, 1}

It pulls β from the right channel of the coproduct to the left, leaving T/β on the right; the disjoint-union product then forms {β, T/β} in the workspace. The grafting step disappears: B(β ⊔ 1) = M(β, 1) = β acts as identity (book p. 50). So

mergeOpUnit β = ⊔ ∘ δ_{β, 1} ∘ Δ^d

with no B step.

Important caveat (book p. 52): "Internal Merge cannot be further decomposed" — M_{β, 1} is not in itself a Merge operation; it only exists as part of the composition (the "virtual particles" analogy on book p. 68). This file gives mergeOpUnit a name for substrate-level algebraic manipulation; that name does NOT signal a stand-alone Merge.

noncomputable def Minimalist.Merge.gammaMatchSingle {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The single-element matching projection γ_{β, 1}: keeps the coefficient of the {β} basis element, sends everything else to zero. Same shape as gammaMatch but with a singleton target.

Equations

• Minimalist.Merge.gammaMatchSingle β = Finsupp.lsingle {β} ∘ₗ Finsupp.lapply {β}

theorem Minimalist.Merge.gammaMatchSingle_apply_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) : (gammaMatchSingle β) (ConnesKreimer.forestToHc F) = if F = {β} then ConnesKreimer.forestToHc F else 0

γ_{β, 1} acts as a basis-vector projection: on forestToHc F, it returns forestToHc F if F = {β}, and 0 otherwise. Singleton counterpart of gammaMatch_apply_singleton.

noncomputable def Minimalist.Merge.deltaMatchSingle {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α) →ₗ[R] TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)

The matching operator δ_{β, 1} on tensored coproduct output: applies gammaMatchSingle β to the left channel, identity to the right.

Equations

• Minimalist.Merge.deltaMatchSingle β = TensorProduct.map (Minimalist.Merge.gammaMatchSingle β) LinearMap.id

noncomputable def Minimalist.Merge.mergePostUnit {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) : TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α) →ₗ[R] ConnesKreimer.Hc R α

Post-coproduct chain for M_{β, 1}: ⊔ ∘ δ_{β, 1}. NO grafting step (book p. 50: B(β ⊔ 1) = β is the identity). Parallel to mergePost for the binary-Merge case.

Equations

• Minimalist.Merge.mergePostUnit β = Minimalist.Merge.hcMulLin ∘ₗ Minimalist.Merge.deltaMatchSingle β

noncomputable def Minimalist.Merge.mergeOpUnit {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) : ConnesKreimer.Hc R α →ₗ[R] ConnesKreimer.Hc R α

The "Merge-with-unit" operator M_{β, 1} per @cite{marcolli-chomsky-berwick-2025} Prop 1.4.2 (book p. 50). The first half of Internal Merge. Factors as mergePostUnit β ∘ comulDelAlgHom.

NOT a Merge operation in its own right: book p. 52 emphasizes "the apparent composite nature is purely illusory" — M_{β,1} only exists as part of M_{T/β, β} ∘ M_{β, 1}, like virtual particles in physics. The name here is a substrate convenience for stating Prop 1.4.2's composition equation algebraically.

Equations

• Minimalist.Merge.mergeOpUnit β = Minimalist.Merge.mergePostUnit β ∘ₗ ConnesKreimer.comulDelAlgHom.toLinearMap

theorem Minimalist.Merge.mergePostUnit_basis_tensor {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) (F : ConnesKreimer.TraceForest α Unit) (r : ConnesKreimer.Hc R α) : (mergePostUnit β) (ConnesKreimer.forestToHc F ⊗ₜ[R] r) = if F = {β} then ConnesKreimer.forestToHc {β} * r else 0

mergePostUnit evaluated on a basis tensor forestToHc F ⊗ r:

• returns forestToHc {β} * r if F = {β}
• returns 0 otherwise.

Singleton counterpart of mergePost_basis_tensor; one fewer step (no graftBinaryAt).

theorem Minimalist.Merge.mergeOpUnit_one {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (β : ConnesKreimer.TraceTree α Unit) : (mergeOpUnit β) 1 = 0

Sanity check: mergeOpUnit β on the empty workspace (1 : Hc R α) is zero. 1 = forestToHc 0 is the multiplicative unit / empty workspace; δ_{β, 1} projects on {β} ≠ 0, so all cuts are killed and only the primitive 1 ⊗ 1 term survives, which also fails the projection. Confirms M-C-B's caveat: M_{β, 1} requires β to be actually present somewhere in the workspace.