Merge operator on the Connes–Kreimer bialgebra of nonplanar forests #
Per [MCB25] §1.3 (Definitions 1.3.1, 1.3.2, 1.3.4),
the linguistic Merge operator M_{S,S'} for a pair (S, S') : Nonplanar α
of accessible terms is the composition
M_{S,S'} = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ
on the canonical carrier ConnesKreimer R (Nonplanar α), where:
Δis the merge coproduct (comulAlgHomN, the Δ^ρ deletion coproduct);δ_{S,S'}selects coproduct terms whose left channel equals the 2-element forest{S, S'}(Def 1.3.1);B ⊗ idgrafts on the left channel: replaces the 2-element forest{S, S'}with the binary treeNonplanar.node lbl {S, S'}(the labellblof the new root is a parameter — the operator layer is agnostic to which label decorates the grafted node);⊔is multiplication onConnesKreimer R (Nonplanar α)(forest disjoint union, the algebra structure).
This file builds the building blocks (gammaMatch, deltaMatch, graftBinaryAt)
and assembles mergeOp. Bridges to linguistic Step.apply live in
Merge.External (EM) and Merge.Internal (IM).
Merge coproduct: Δ^ρ, not Δ^d #
[MCB25] Def 1.3.4 states merge with the Δ^d
(delete-then-rebinarize) coproduct. The canonical n-ary carrier uses Δ^ρ
(comulAlgHomN): Δ^d and Δ^ρ extract the same accessible terms, differing
only in the remainder, which mergePost discards when grafting the pair — so
merge correctness is unaffected. Δ^ρ is the n-ary-faithful deletion (MCB's
binary Δ^d +2 is a rebinarization artifact).
The cost-weighted Merge M^ε (eq. 1.5.1) is deferred: it needs an
ε-weighted Δ^ρ (a cutTotalDepth analogue on cutSummandsN), not yet in the
substrate.
§1: γ_{S,S'} matching projection (M-C-B Def 1.3.1) #
For a fixed pair (S, S') : Nonplanar α, gammaMatch S S' is the linear
endomorphism of ConnesKreimer R (Nonplanar α) that projects onto the basis
element of' {S, S'}:
gammaMatch S S' (of' F) = if F = {S, S'} then of' F else 0
Built as a ConnesKreimer.linearLift that maps the {S, S'} basis vector to
itself and every other basis vector to zero.
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' = RootedTree.ConnesKreimer.linearLift fun (F : RootedTree.Forest (RootedTree.Nonplanar α)) => if F = {S, S'} then RootedTree.ConnesKreimer.of' F else 0
Instances For
γ_{S,S'} acts as a basis-vector projection: on the basis element
of' F, it returns of' 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 the coproduct output.
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
Instances For
§3: B grafting for binary Merge (M-C-B Def 1.3.2 + Lemma 1.3.3) #
graftBinaryAt lbl S S' replaces the 2-element forest {S, S'} (basis element)
with the binary tree Nonplanar.node lbl {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.
The label lbl of the grafted root is a parameter: the operator layer is
agnostic to which label decorates the new node (consumers supply the lexical
head).
The grafting operator B specialized at the pair (S, S') with root label
lbl: maps the basis element {S, S'} to Nonplanar.node lbl {S, S'}, all
other basis elements to zero. M-C-B Lemma 1.3.3 for binary Merge.
Equations
- One or more equations did not get rendered due to their size.
Instances For
B grafts on basis vectors: on of' F, returns
of' {Nonplanar.node lbl {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 lbl S S' = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ^ρ
The chain:
Δ^ρ(comulAlgHomN) extracts accessible cuts (deletion remainder)δ_{S,S'}filters to terms where the cut forest equals{S, S'}(B ⊗ id)grafts{S, S'}intoNonplanar.node lbl {S, S'}on the left⊔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 lbl S S' F = 0.
Multiplication on ConnesKreimer R (Nonplanar α) lifted to a linear map.
Wraps mathlib's Algebra.TensorProduct.lmul'.
Equations
- Minimalist.Merge.mulLin = (Algebra.TensorProduct.lmul' R).toLinearMap
Instances For
Post-coproduct chain ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} as a single named linear
map. mergeOp factors as mergePost lbl S S' ∘ comulAlgHomN.toLinearMap.
Equations
- Minimalist.Merge.mergePost lbl S S' = Minimalist.Merge.mulLin ∘ₗ TensorProduct.map (Minimalist.Merge.graftBinaryAt lbl S S') LinearMap.id ∘ₗ Minimalist.Merge.deltaMatch S S'
Instances For
The Merge operator M_{S,S'} per M-C-B Def 1.3.4 (with root label lbl).
Factors as mergePost lbl S S' ∘ comulAlgHomN.
Equations
- Minimalist.Merge.mergeOp lbl S S' = Minimalist.Merge.mergePost lbl S S' ∘ₗ RootedTree.ConnesKreimer.comulAlgHomN.toLinearMap
Instances For
§5: Post-coproduct chain on basis tensors #
mergePost lbl S S' evaluated on an elementary tensor of' F ⊗ r is:
of' {Nonplanar.node lbl {S, S'}} * rifF = {S, S'}0otherwise
This is the load-bearing fact for proving algebraic Merge agrees with
linguistic Step.apply: every basis-tensor term in the coproduct expansion of
Δ^ρ({S, S'}) either matches the merge target or is annihilated by δ_{S,S'}.
The post-coproduct chain mergePost lbl S S' evaluated on a basis tensor
of' F ⊗ r.
General γ_{S,S'}-vanishing on a left-multiplied forest: if F is NOT a
sub-multiset of {S, S'}, then γ_{S,S'}(of' F * a) = 0 for any a.
The hypothesis ¬ F ≤ ({S, S'} : Forest (Nonplanar α)) says F cannot
embed into {S, S'} as a sub-multiset: since F ≤ F + G always, every
forest F + G produced by left-multiplication misses the {S, S'} basis
element that γ_{S,S'} reads.
Disjoint-singleton vanishing of γ_{S,S'} (corollary): if T ≠ S and
T ≠ S', then γ_{S,S'}(of' {T} * a) = 0.
Vanishing of mergePost on left-multiplied disjoint factors: if F is NOT
a sub-multiset of {S, S'} and b is arbitrary, then for any z:
mergePost lbl S S' ((of' F ⊗ b) * z) = 0.
Eliminates cross-terms in the F̂-residual generalization of mergeOp_pair:
any term whose LEFT contribution is a forest F that doesn't fit inside
{S, S'} vanishes after mergePost.
Right-multiplicativity of the post-coproduct chain by a "pure
right-channel" factor 1 ⊗ y. For any z and any y:
mergePost lbl S S' (z * (1 ⊗ y)) = mergePost lbl S S' z * y.
Load-bearing for the F̂-residual generalization of mergeOp_pair: the
all-empty-cut term of the residual coproduct has the form 1 ⊗ F̂, so this
propagates the residual workspace through the chain unchanged.
§6: M_{β, 1} substrate (single-element matching, no grafting) #
Per [MCB25] §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} ∘ Δ^ρ
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. This file gives mergeOpUnit a name for substrate-level algebraic
manipulation; that name does NOT signal a stand-alone Merge.
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 β = RootedTree.ConnesKreimer.linearLift fun (F : RootedTree.Forest (RootedTree.Nonplanar α)) => if F = {β} then RootedTree.ConnesKreimer.of' F else 0
Instances For
γ_{β, 1} acts as a basis-vector projection: on of' F, returns of' F
if F = {β}, and 0 otherwise. Singleton counterpart of
gammaMatch_apply_singleton.
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
Instances For
Post-coproduct chain for M_{β, 1}: ⊔ ∘ δ_{β, 1}. NO grafting step
(book p. 50: B(β ⊔ 1) = β is the identity). Parallel to mergePost.
Equations
Instances For
The "Merge-with-unit" operator M_{β, 1} per
[MCB25] Prop 1.4.2 (book p. 50). The first half of
Internal Merge. Factors as mergePostUnit β ∘ comulAlgHomN.
NOT a Merge operation in its own right (book p. 52): only exists as part of
M_{T/β, β} ∘ M_{β, 1}. The name is a substrate convenience for stating
Prop 1.4.2's composition equation algebraically.
Equations
Instances For
mergePostUnit evaluated on a basis tensor of' F ⊗ r:
- returns
of' {β} * rifF = {β} - returns
0otherwise.
Singleton counterpart of mergePost_basis_tensor; one fewer step.
Sanity check: mergeOpUnit β on the empty workspace (1 : ConnesKreimer R (Nonplanar α)) is zero. 1 = of' 0 is the multiplicative unit / empty
workspace; δ_{β, 1} projects on {β} ≠ 0, so all cuts are killed.
Confirms M-C-B's caveat: M_{β, 1} requires β to be present.