⚠️ LEGACY — RESTORED SHIM (2026-05-13)

Restored from commit e0876460^ after deletion at 0.230.913. Will be re-deleted when Phase D lands per scratch/mcb_full_architecture.md: general n-ary Δ^c via cuts-of-cuts on RootedTree α [Inhabited α]. Canonical replacement substrate: Linglib/Core/Algebra/RootedTree/Coproduct/Trace.lean (comulCAlgHomP etc.) — currently planar-only and operates on Planar (α ⊕ β) rather than the binary Hc R α := AddMonoidAlgebra R (TraceForest α Unit) carrier this file provides.

Do not extend, do not add new consumers.

---

Connes-Kreimer Coproduct on the Bialgebra of Trace-Anonymized Forests

@cite{marcolli-chomsky-berwick-2025}

Per @cite{marcolli-chomsky-berwick-2025} Definition 1.2.8, the contraction coproduct on the syntactic forest bialgebra is

Δ^c(T) := T ⊗ 1 + 1 ⊗ T + Σ_{F_v} F_v ⊗ T/^c F_v

where the sum is over all subforests F_v ⊂ T consisting of disjoint accessible terms of T, and T/^c F_v is the contraction-with-trace remainder (Definition 1.2.4).

Equivalently, identifying the empty cut with the 1 ⊗ T term:

Δ^c(T) = T ⊗ 1 + Σ_{c : CutShape T} (cutForest c) ⊗ (remainder c)

Carrier: TraceTree α Unit (not DecoratedTree α)

This file builds Δ^c on TraceTree α Unit (the trace-anonymized carrier), NOT on DecoratedTree α (the linguistic-data carrier). Per @cite{marcolli-skigin-2025} §10.1, the bialgebra structure requires trace labels to be scalars from a disjoint marked copy of the leaf alphabet (specialized here to β = Unit), not recursive subtrees. The bialgebra instance lives on the object whose elements are the equivalence classes — i.e., on the trace-anonymized carrier — per the mathlib idiom that algebraic structures live on quotients, not on preimages with projections.

Linguistic-layer code that maintains DecoratedTree α data should project via Forest.anon (fun _ => ()) at the boundary before invoking comulAlgHom. See Decorated.lean for the projection.

This file builds:

• comulTree T : Hc ⊗[R] Hc — the tree-level coproduct
• comulForest F : Hc ⊗[R] Hc — extension to forests by multiplicativity (Δ^c on a forest = product of Δ^c on components, per M-C-B Δ^ω(F) = ⊔_a Δ(T_a))
• comulAlgHom : Hc →ₐ[R] Hc ⊗[R] Hc — algebra-hom lift via AddMonoidAlgebra.lift (the algebra-hom property is needed for the bialgebra structure per M-C-B Lemma 1.2.10)
• counit : Hc →ₐ[R] R — the counit (algebra hom selecting the empty-forest coefficient)
• comulDelAlgHom : Hc →ₐ[R] Hc ⊗[R] Hc — the deletion coproduct Δ^d used by the linguistic Merge action

Naming note: we use comulAlgHom rather than comul to leave the short name comul available for the eventual Coalgebra typeclass instance field (which takes Hc →ₗ[R] Hc ⊗ Hc, the linear-map projection of comulAlgHom.toLinearMap).

The Coalgebra/Bialgebra typeclass instances are NOT declared here — that's a separate file once coassoc is proven (Foissy-style cuts-of- cuts bijection or via Lemma 1.2.10's appeal to Connes-Kreimer for Feynman graphs). The Hopf algebra structure requires the additional quotient by (1 - α) for α ∈ SO_0 per Lemma 1.2.10.

Layer status

[UPSTREAM] candidate. Future home is something like Mathlib.Combinatorics.HopfAlgebra.ConnesKreimer.Coproduct. This file is part of the Stage 0.5 hoist out of Theories/Syntax/Minimalist/Hopf/ (per scratch/mcb_stage1_plan.md).

Mathlib infra leveraged

• Hc = AddMonoidAlgebra R (TraceForest α Unit) = (TraceForest α Unit →₀ R) (from Defs.lean)
• TensorProduct R Hc Hc with ⊗ₜ notation
• Finsupp.single F z : Hc for basis elements (F : TraceForest α Unit)
• Finsupp.linearCombination for linear extension from a function on basis elements
• Multiset.prod for the multiplicative-on-forests extension
• Finsupp.lapply for the counit (value at the empty-forest index)

§1: Tree-level coproduct

For a single tree T : TraceTree α Unit, define the contraction coproduct as the explicit primitive T ⊗ 1 plus the sum over admissible cuts:

Δ^c(T) = T ⊗ 1 + Σ_{c : CutShape T} (single (cutForest c)) ⊗ (single {remainder c})

The empty cut CutShape.empty T contributes the 1 ⊗ T term (cutForest = ∅, remainder = T). The explicit T ⊗ 1 corresponds to M-C-B's "T as a member of the workspace [T]" primitive — not an admissible cut, since there is no edge above the root to remove.

noncomputable def ConnesKreimer.forestToHc {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : Hc R α

Inject a forest into the bialgebra as a basis element. The singleton-workspace embedding for a single tree T is forestToHc {T}. Takes TraceForest α Unit (the bialgebra carrier basis); for Forest α-bearing callers, project via Forest.anon (fun _ => ()) first.

Equations

• ConnesKreimer.forestToHc F = Finsupp.single F 1

@[simp]

theorem ConnesKreimer.forestToHc_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : forestToHc 0 = 1

The empty forest embeds as the multiplicative unit: forestToHc 0 = (1 : Hc R α). Direct from AddMonoidAlgebra.one_def.

@[simp]

theorem ConnesKreimer.forestToHc_add {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F G : TraceForest α Unit) : forestToHc (F + G) = forestToHc F * forestToHc G

Disjoint union of forests corresponds to multiplication of their forestToHc images: forestToHc (F + G) = forestToHc F * forestToHc G. Direct from AddMonoidAlgebra.single_mul_single at coefficient 1.

noncomputable def ConnesKreimer.comulTreeFiltered {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) (P : CutShape T → Bool) : TensorProduct R (Hc R α) (Hc R α)

The filtered tree-level Connes-Kreimer coproduct: same shape as comulTree but the cut-set sum is restricted to cuts satisfying a Boolean predicate P. The primitive T ⊗ 1 term is always retained.

Common subsumed cases (each is comulTreeFiltered T P for some P):

• comulTree T = comulTreeFiltered T (fun _ => true) (unrestricted Δ^c).
• comulPhaseC h T ℓ (in Merge/PhaseCoproduct.lean) = comulTreeFiltered T.toHc (cutPhaseCompatible h T ℓ) (Δ^c_Φ).
• Future cost-restricted, complexity-restricted, feature-restricted coproducts can all use the same primitive.

Decoupling the filtering predicate from the carrier lets consumers state "unrestricted limit recovery" lemmas (e.g., comulTreeFiltered T (fun _ => true) = comulTree T is rfl modulo Finset.filter_true).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.comulTree {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : TensorProduct R (Hc R α) (Hc R α)

The tree-level Connes-Kreimer coproduct. Δ^c(T) = T ⊗ 1 + Σ_c (cutForest c) ⊗ ({remainder c}).

Defined as the unrestricted (filter-true) case of comulTreeFiltered.

Equations

• ConnesKreimer.comulTree T = ConnesKreimer.comulTreeFiltered T fun (x : ConnesKreimer.CutShape T) => true

@[simp]

theorem ConnesKreimer.comulTreeFiltered_true {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : (comulTreeFiltered T fun (x : CutShape T) => true) = comulTree T

Recovery: when the filter is constantly true, comulTreeFiltered reduces to comulTree.

theorem ConnesKreimer.comulTree_eq_prim_add_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : comulTree T = forestToHc {T} ⊗ₜ[R] 1 + ∑ c : CutShape T, forestToHc c.cutForest ⊗ₜ[R] forestToHc {c.remainder}

Structural decomposition of comulTree T into the explicit primitive T ⊗ 1 term plus the unfiltered sum over admissible cuts. Direct from the definition (comulTree := comulTreeFiltered _ true, Finset.filter_true_of_mem makes the filter trivial).

§2: Forest-level coproduct (multiplicative extension)

Per M-C-B equation just above (1.2.10): "The coproduct (1.2.8) is extended to forests F = ⊔_a T_a in the form Δ^ω(F) = ⊔_a Δ(T_a)."

Multiplication on Hc ⊗ Hc is the tensor-product algebra multiplication, which gives (a ⊗ b) * (c ⊗ d) = (a*c) ⊗ (b*d). On basis elements this is single F₁ ⊗ single G₁ * single F₂ ⊗ single G₂ = single (F₁ + F₂) ⊗ single (G₁ + G₂). So the multiplicative extension correctly distributes ⊔ on both channels.

noncomputable def ConnesKreimer.comulForest {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : TensorProduct R (Hc R α) (Hc R α)

The forest-level Connes-Kreimer coproduct: product of tree-level coproducts over the components of the forest.

Equations

• ConnesKreimer.comulForest F = (Multiset.map ConnesKreimer.comulTree F).prod

§3: Multiplicativity of comulForest

Per M-C-B (text just above Lemma 1.2.10): the coproduct on a forest is the product of coproducts on its components. With comulForest defined as Multiset.prod (F.map comulTree), this is structurally true: Multiset.prod is multiplicative under + ↦ +/map ↦ map.

@[simp]

theorem ConnesKreimer.comulForest_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : comulForest 0 = 1

@[simp]

theorem ConnesKreimer.comulForest_add {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F G : TraceForest α Unit) : comulForest (F + G) = comulForest F * comulForest G

§4: Algebra-hom lift to Hc

AddMonoidAlgebra.lift R A M is the canonical equivalence (Multiplicative M →* A) ≃ (R[M] →ₐ[R] A). We construct the multiplicative-monoid hom from comulForest and then lift to get an algebra hom Hc R α →ₐ[R] Hc R α ⊗ Hc R α. The algebra-hom property is exactly what's needed for the bialgebra structure per M-C-B Lemma 1.2.10.

noncomputable def ConnesKreimer.comulMonoidHom {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Multiplicative (TraceForest α Unit) →* TensorProduct R (Hc R α) (Hc R α)

comulForest, packaged as a Multiplicative (TraceForest α Unit) →* (Hc R α ⊗[R] Hc R α) monoid hom. Multiplication on Multiplicative (TraceForest α Unit) corresponds to addition on TraceForest α Unit (disjoint union ⊔).

Public (not private) so Bialgebra.lean's helper lemma comulAlgHom_apply_single can reference it. Downstream callers should generally use comulAlgHom (the AlgHom-shaped public API) rather than this monoid hom directly.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.comulAlgHom {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Hc R α →ₐ[R] TensorProduct R (Hc R α) (Hc R α)

The Connes-Kreimer coproduct on the bialgebra of trace-anonymized forests, as an algebra hom. M-C-B Definition 1.2.8 (with ω = c).

Naming: short name comul is reserved for the eventual Coalgebra typeclass instance field, which takes the linear-map projection comulAlgHom.toLinearMap.

Equations

• ConnesKreimer.comulAlgHom = (AddMonoidAlgebra.lift R (TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)) (ConnesKreimer.TraceForest α Unit)) ConnesKreimer.comulMonoidHom

@[simp]

theorem ConnesKreimer.comulAlgHom_apply_single {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : comulAlgHom (Finsupp.single F 1) = comulForest F

comulAlgHom applied to the basis vector Finsupp.single F 1 equals comulForest F. Follows from AddMonoidAlgebra.lift_single.

§5: Counit (also an algebra hom)

The counit ε : Hc R α → R extracts the coefficient of the empty forest. For the bialgebra structure it must be an algebra hom; the underlying monoid hom is F ↦ if F = 0 then 1 else 0, which is multiplicative because F + G = 0 ↔ F = 0 ∧ G = 0 for multisets.

noncomputable def ConnesKreimer.counitMonoidHom {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Multiplicative (TraceForest α Unit) →* R

The counit, as a Multiplicative (TraceForest α Unit) →* R monoid hom. Public so Bialgebra.lean's helper lemma counit_apply_single can reference it; downstream callers should generally use counit (the AlgHom-shaped public API).

Equations

• ConnesKreimer.counitMonoidHom = { toFun := fun (F : Multiplicative (ConnesKreimer.TraceForest α Unit)) => if Multiplicative.toAdd F = 0 then 1 else 0, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def ConnesKreimer.counit {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Hc R α →ₐ[R] R

The counit on the bialgebra of trace-anonymized forests, as an algebra hom.

Equations

• ConnesKreimer.counit = (AddMonoidAlgebra.lift R R (ConnesKreimer.TraceForest α Unit)) ConnesKreimer.counitMonoidHom

§6: Δ^d (deletion coproduct)

Per M-C-B Def 1.2.8 with ω = d, Δ^d uses remainderDeletion (removal + rebinarization) instead of remainder (contraction with trace). Δ^d is what the linguistic Merge action uses (Definition 1.3.4 p. 42, "consider the coproduct Δ = Δ^d"). Algebraically Δ^d satisfies a weaker coassoc relation than Δ^c (per Lemma 1.2.12, multiplicities differ at distance ≤ 1), but it's still multiplicative on forests, so the algebra-hom lift works the same way.

When remainderDeletion c = none (the cut consumed the entire root component — only happens for CutShape.bothCut), the right channel of the coproduct term becomes 1 (the empty workspace).

noncomputable def ConnesKreimer.deletionRightChannel {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (m : Option (TraceTree α Unit)) : Hc R α

Helper: convert an Option (TraceTree α Unit) remainder to the corresponding right-channel value in Hc R α. Option.none → (1 : Hc R α) (empty workspace); Option.some t → forestToHc {t} (singleton workspace).

Public because comulTreeDel_eq_prim_add_sum (the structural decomposition lemma below) names it in its statement: any consumer that uses that lemma to destructure comulTreeDel summands needs the symbol to be in scope.

Equations

• ConnesKreimer.deletionRightChannel none = 1
• ConnesKreimer.deletionRightChannel (some t) = ConnesKreimer.forestToHc {t}

noncomputable def ConnesKreimer.comulTreeDel {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : TensorProduct R (Hc R α) (Hc R α)

The tree-level Δ^d coproduct. Δ^d(T) = T ⊗ 1 + Σ_c (cutForest c) ⊗ (deletion-remainder c).

Equations

• One or more equations did not get rendered due to their size.

theorem ConnesKreimer.comulTreeDel_eq_prim_add_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : comulTreeDel T = forestToHc {T} ⊗ₜ[R] 1 + ∑ c : CutShape T, forestToHc c.cutForest ⊗ₜ[R] deletionRightChannel c.remainderDeletion

The structural decomposition of comulTreeDel T into its primitive T ⊗ 1 term and the sum of admissible-cut terms. Stated as a named rfl lemma so downstream proofs (e.g., the algebraic Merge bridge in Theories/Syntax/Minimalist/Merge/Action.lean) are robust under refactors of comulTreeDel's body. Lives in ConnesKreimer (where deletionRightChannel is in scope) rather than at the consumer.

§6.5: Cost-weighted Δ^d for Minimal Search

@cite{marcolli-chomsky-berwick-2025} §1.5

Per @cite{marcolli-chomsky-berwick-2025} rules 1-5, p. 59 + eq. (1.5.1)-(1.5.2) (§1.5.2 / §1.5.3), the cost-weighted Merge operator M^ε_{S, S'} weights each admissible cut's contribution by ε^{depth}. At the coproduct layer this corresponds to weighting comulTreeDel's cut sum by ε^{cutTotalDepth c}.

comulTreeDel_eps ε T is the ε-parameterized version. Two key facts:

• At ε = 1: weights collapse to 1, recovering comulTreeDel T.
• At ε = 0: only cost-0 contributions (= empty cut, by 7d.1's cutTotalDepth_eq_zero_of_cutForest_eq_zero) survive, leaving just the primitive part T ⊗ 1 + 1 ⊗ T. This matches M-C-B Remark 1.3.8 (p. 47): "External Merge picks out the primitive part of the coproduct."

Phase 7d's punchline: in the ε → 0 limit, mergeOp_eps 0 produces only Case 1 of §1.4.1 (External Merge member-level matching), automatically suppressing all Sideward Merge contributions. This DERIVES the disjointness hypothesis from mergeOp_pair_residual rather than stipulating it.

noncomputable def ConnesKreimer.comulTreeDel_eps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) (T : TraceTree α Unit) : TensorProduct R (Hc R α) (Hc R α)

The ε-weighted tree-level Δ^d coproduct. Each cut c contributes its usual term scaled by ε^{cutTotalDepth c}. The primitive T ⊗ 1 term has cost 0 (no extraction) and is unweighted.

Equations

• One or more equations did not get rendered due to their size.

theorem ConnesKreimer.comulTreeDel_eps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : comulTreeDel_eps 1 T = comulTreeDel T

At ε = 1, the weighted coproduct collapses to the unweighted one (since 1^n = 1 and 1 • x = x).

theorem ConnesKreimer.comulTreeDel_eps_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : comulTreeDel_eps 0 T = forestToHc {T} ⊗ₜ[R] 1 + 1 ⊗ₜ[R] forestToHc {T}

At ε = 0, only the empty cut's contribution survives the weighting (since 0^0 = 1 and 0^k = 0 for k ≥ 1). The empty cut has cutForest = 0 and remainderDeletion = some T, so its contribution is 1 ⊗ forestToHc {T}. Combined with the unweighted primitive T ⊗ 1, the result is the primitive part of M-C-B Remark 1.3.8.

noncomputable def ConnesKreimer.comulForestDel {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : TensorProduct R (Hc R α) (Hc R α)

The forest-level Δ^d coproduct: product of tree-level coproducts over the components. Same multiplicative extension as Δ^c.

Equations

• ConnesKreimer.comulForestDel F = (Multiset.map ConnesKreimer.comulTreeDel F).prod

@[simp]

theorem ConnesKreimer.comulForestDel_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : comulForestDel 0 = 1

@[simp]

theorem ConnesKreimer.comulForestDel_add {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F G : TraceForest α Unit) : comulForestDel (F + G) = comulForestDel F * comulForestDel G

noncomputable def ConnesKreimer.comulForestDel_eps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) (F : TraceForest α Unit) : TensorProduct R (Hc R α) (Hc R α)

The ε-weighted forest-level Δ^d coproduct: product of comulTreeDel_eps ε across components. Joint-cut weights multiply: ε^{Σ d_i} = ∏ ε^{d_i}.

Equations

• ConnesKreimer.comulForestDel_eps ε F = (Multiset.map (ConnesKreimer.comulTreeDel_eps ε) F).prod

@[simp]

theorem ConnesKreimer.comulForestDel_eps_zero_forest {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) : comulForestDel_eps ε 0 = 1

@[simp]

theorem ConnesKreimer.comulForestDel_eps_add {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) (F G : TraceForest α Unit) : comulForestDel_eps ε (F + G) = comulForestDel_eps ε F * comulForestDel_eps ε G

theorem ConnesKreimer.comulForestDel_eps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : comulForestDel_eps 1 F = comulForestDel F

At ε = 1, the weighted forest coproduct collapses to the unweighted one.

noncomputable def ConnesKreimer.comulDelMonoidHom_eps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) : Multiplicative (TraceForest α Unit) →* TensorProduct R (Hc R α) (Hc R α)

comulForestDel_eps ε, packaged as a multiplicative monoid hom.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.comulDelAlgHom_eps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) : Hc R α →ₐ[R] TensorProduct R (Hc R α) (Hc R α)

The ε-weighted Δ^d coproduct as an algebra hom Hc R α →ₐ[R] Hc R α ⊗ Hc R α. Parallel to comulDelAlgHom; collapses at ε = 1.

Equations

• One or more equations did not get rendered due to their size.

theorem ConnesKreimer.comulDelAlgHom_eps_apply_single {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (ε : R) (F : TraceForest α Unit) : (comulDelAlgHom_eps ε) (Finsupp.single F 1) = comulForestDel_eps ε F

comulDelAlgHom_eps ε on the basis vector Finsupp.single F 1 equals comulForestDel_eps ε F. Analog of comulDelAlgHom_apply_single.

noncomputable def ConnesKreimer.comulDelMonoidHom {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Multiplicative (TraceForest α Unit) →* TensorProduct R (Hc R α) (Hc R α)

comulForestDel, packaged as a multiplicative monoid hom. Public so consistency with comulMonoidHom / counitMonoidHom (also public to support Bialgebra.lean helper lemmas). Downstream callers should generally use comulDelAlgHom (the AlgHom-shaped public API).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.comulDelAlgHom {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : Hc R α →ₐ[R] TensorProduct R (Hc R α) (Hc R α)

The Δ^d coproduct as an algebra hom Hc R α →ₐ[R] Hc R α ⊗ Hc R α. M-C-B Definition 1.2.8 with ω = d. This is the coproduct used by the action of Merge per Definition 1.3.4 (p. 42).

Δ^d is NOT a coassociative coalgebra in the standard sense. M-C-B Lemma 1.2.12 (p. 39) proves only that the terms of (1 ⊗ Δ^d) ∘ Δ^d(T) and (Δ^d ⊗ 1) ∘ Δ^d(T) match for cuts at distance ≤ 1 — but they appear "with different multiplicity" (Figure 1.3, p. 40), and pairs at distance > 1 differ. Remark 1.2.9 (p. 34) explicitly calls this "a weaker version of the coassociativity relation". The proper algebraic structure for Δ^d is deferred by M-C-B to Marcolli-Walton ("Generalized Quasi-Hopf Algebras and Merge", in preparation, ref [146]).

Hence comulDelAlgHom is NOT registered as Bialgebra.comul for Hc R α. The instBialgebraHc typeclass uses comulAlgHom (= Δ^c, Connes-Kreimer canonical, Foissy 2002 ref [19]); see Bialgebra.lean.

Derivation from Δ^c (M-C-B p. 44): Δ^d can be expressed as Δ^d = (id ⊗ Π_{d,c}) ∘ Δ^c where Π_{d,c} is the linear projection that removes .trace markers and edge-contracts. We currently define comulDelAlgHom directly (parallel to comulAlgHom) rather than deriving it via this projection — see TODO note in Bialgebra.lean for the future refactor.

Δ^d is consumed by Minimalism's Merge operator (Theories/Syntax/Minimalist/Merge/Basic.lean); it does NOT participate in the Bialgebra typeclass mediation.

Equations

• ConnesKreimer.comulDelAlgHom = (AddMonoidAlgebra.lift R (TensorProduct R (ConnesKreimer.Hc R α) (ConnesKreimer.Hc R α)) (ConnesKreimer.TraceForest α Unit)) ConnesKreimer.comulDelMonoidHom

theorem ConnesKreimer.comulDelAlgHom_apply_single {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : TraceForest α Unit) : comulDelAlgHom (Finsupp.single F 1) = comulForestDel F

comulDelAlgHom applied to the basis vector Finsupp.single F 1 equals comulForestDel F. Analog of comulAlgHom_apply_single.

Not @[simp]: AddMonoidAlgebra.lift_single already fires on this LHS leaving comulDelMonoidHom F.toAdd, and rewriting through this lemma jumps several normalization steps in one move — fragile if callers are reasoning about partial unfoldings. Invoke explicitly.

@[simp]

theorem ConnesKreimer.comulForestDel_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T : TraceTree α Unit) : comulForestDel {T} = comulTreeDel T

comulForestDel on the singleton forest {T} reduces to comulTreeDel T.

theorem ConnesKreimer.comulDelAlgHom_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (T1 T2 : TraceTree α Unit) : comulDelAlgHom (forestToHc {T1, T2}) = comulTreeDel T1 * comulTreeDel T2

Δ^d on a 2-tree workspace (M-C-B Def 1.2.8 with ω = d, applied to F = {T1, T2}). Multiplicativity of comulDelAlgHom gives Δ^d({T1, T2}) = Δ^d(T1) · Δ^d(T2) — the load-bearing fact for the algebraic Merge bridge in Theories/Syntax/Minimalist/Merge/External.lean.

theorem ConnesKreimer.comulDelAlgHom_eps_one_eq {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : comulDelAlgHom_eps 1 = comulDelAlgHom

At ε = 1, the weighted algebra hom collapses to the unweighted one: comulDelAlgHom_eps 1 = comulDelAlgHom. By AddMonoidAlgebra.algHom_ext, suffices to verify on basis vectors single F 1.