Documentation

Linglib.Core.Algebra.ConnesKreimer.Defs

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

Restored from commit e0876460^ after deletion at 0.230.913 ("MCB substrate Phase A.5-A.6 + hard delete of legacy CK substrate"). Consumer migration (Phase D per scratch/mcb_full_architecture.md) hadn't happened; Merge stack files broke on clean build. Will be re-deleted when Phase D lands (general n-ary Δ^c on RootedTree α [Inhabited α], consumers using RootedTree.ConnesKreimer R T).

Do not extend, do not add new consumers.

Bialgebra Carrier of Decorated Forests @cite{marcolli-chomsky-berwick-2025} #

The R-linear free module on TraceForest α Unit (multisets of trace-anonymized trees), with multiplication = disjoint union of forests. This is the underlying carrier of the Connes-Kreimer-style bialgebra of decorated rooted trees.

Per @cite{marcolli-chomsky-berwick-2025} Lemma 1.2.10, the contraction coproduct (next file: Coproduct.lean) gives Hc the structure of a graded commutative bialgebra — but NOT (yet) a Hopf algebra. The Hopf algebra arises only after quotienting by the ideal generated by 1 - α for α ∈ SO_0 (the leaves are degree-0 group-like elements lacking inverses, which prevents the antipode from existing on Hc itself). The eventual Hopf algebra is on the quotient Hc / (1 - α).

On the basis: TraceForest α Unit (not Forest α) #

The basis-key type was originally Forest α := Multiset (DecoratedTree α). But DecoratedTree's .trace t constructor carries the contracted subtree t as data, and treating that data literally as part of the basis-element key breaks coassociativity: iterated coproducts produce .trace _ markers whose contents differ between iteration orders, even though the underlying combinatorial 3-coloring matches. (Counterexample: scratch/SlotThreeMismatch.lean.)

@cite{marcolli-skigin-2025} §10.1 ("Labels of traces of movement") addresses this: trace labels need to be scalars, not recursive subtrees, so iterated traces resolve to the same label as the original subtree. We realize this by keying the bialgebra basis on TraceForest α Unit (see RootedTree/Decorated.lean for TraceTree α β), with the trivial extractor fun _ => () projecting .trace t to TraceTree.trace (). The polymorphic TraceTree α β remains available for richer linguistic labels (e.g., β = α for M-S-aligned head labels) without disturbing this Hopf algebra layer.

On def Hc, not abbrev Hc #

Hc R α is a def (not abbrev) for AddMonoidAlgebra R (TraceForest α Unit). This is the mathlib-canonical pattern (cf. Mathlib.Algebra.MonoidAlgebra.Defs where MonoidAlgebra R M : Type _ := M →₀ R is also def, generated to AddMonoidAlgebra via to_additive_dont_translate): the wrapper def keeps the typeclass slot unique to our Connes-Kreimer Bialgebra instance (registered in Bialgebra.lean via Bialgebra.ofAlgHom), preventing conflict with mathlib's AddMonoidAlgebra.instBialgebra group-like default (Δ(F) = F ⊗ F) which would otherwise fire automatically and give the wrong coproduct.

The mathlib pattern: a def-wrapped algebra type forwards needed foundational instances (Algebra, FunLike) manually so the typeclass slot for the discriminated structure (Bialgebra, here) is unambiguous. We forward only CommSemiring (which auto-derives Semiring), Algebra, FunLike — keeping the surface minimal.

Layer status #

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

Naming TODO (Stage 1.7 or upstream): the one-letter Hc violates mathlib naming hygiene. Rename to ConnesKreimerHc R α or similar when upstreaming.

source
def ConnesKreimer.Hc (R : Type u_1) [CommSemiring R] (α : Type u_2) [DecidableEq α] :
Type (max u_2 u_1)

The bialgebra carrier: formal R-linear combinations of trace-anonymized forests TraceForest α Unit.

def (not abbrev) per the mathlib MonoidAlgebra pattern: the wrapper keeps the typeclass slot unique to our Connes-Kreimer Bialgebra instance (in Bialgebra.lean), preventing conflict with mathlib's group-like default. See module docstring.

Equations
Instances For

    Mathlib instances forwarded for Hc R α #

    Since Hc is def, mathlib instances on AddMonoidAlgebra R (TraceForest α Unit) need explicit forwarding to be visible on Hc R α. Minimal surface: CommSemiring auto-derives Semiring; Ring/CommRing not forwarded (no current consumers requires [CommRing R]).

    source
    @[implicit_reducible]
    noncomputable instance ConnesKreimer.instCommSemiring (R : Type u_1) [CommSemiring R] (α : Type u_2) [DecidableEq α] :
    CommSemiring (Hc R α)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    noncomputable instance ConnesKreimer.instAlgebra (R : Type u_1) [CommSemiring R] (α : Type u_2) [DecidableEq α] :
    Algebra R (Hc R α)
    Equations
    source
    @[implicit_reducible]
    instance ConnesKreimer.instFunLike (R : Type u_1) [CommSemiring R] (α : Type u_2) [DecidableEq α] :
    FunLike (Hc R α) (TraceForest α Unit) R

    Forward the Finsupp.funLike instance so that elements of Hc R α can be applied as functions TraceForest α Unit → R. Needed for counit and other finsupp-flavored lemmas.

    Equations