Bialgebra of Decorated Forests: Linguistic Specialization

@cite{marcolli-chomsky-berwick-2025}

The [LINGLIB] half of the original Hopf/Defs.lean (renamed to Merge/Defs.lean at 0.230.770 along with the Hopf/ → Merge/ dissolve): specialization of the generic Connes-Kreimer substrate (in Core/, namespace ConnesKreimer) to the Minimalism instantiation with α := LIToken, plus the bridge to plain SyntacticObject via the toSyntacticObject? forgetful map.

Where the substrate lives

The [UPSTREAM] portions are in:

• Linglib/Core/Combinatorics/RootedTree/Decorated.lean — ConnesKreimer.TraceTree α Unit, ConnesKreimer.TraceForest α Unit, Mul instance, recOnMul, leafCount*
• Linglib/Core/Combinatorics/RootedTree/AdmissibleCut.lean — ConnesKreimer.CutShape T and friends
• Linglib/Core/Algebra/ConnesKreimer/Defs.lean — ConnesKreimer.Hc R α := AddMonoidAlgebra R (TraceForest α Unit) + Algebra/ Semiring forwarding instances
• Linglib/Core/Algebra/ConnesKreimer/Coproduct.lean — ConnesKreimer.{forestToHc, comulAlgHom, comulDelAlgHom, counit}

This file (and Merge/Basic.lean, Merge/Action.lean) bring those into scope via open ConnesKreimer.

Linguistic specialization

SyntacticObjectH := DecoratedTree LIToken is the Minimalism-side alias (M-C-B §1.1.2 + Def 1.2.4 with leaf type LIToken). The forgetful maps SyntacticObject.toH (lossless embed of plain SO into the Hopf side) and treeToSyntacticObject? (option-valued projection back, returning none if any trace leaf survives) bridge the two encodings.

The treeToSyntacticObject?_ofSO round-trip theorem confirms trace-free SOs survive embedding-then-projection.

Linguistic specialization to α := LIToken

@[reducible, inline]

abbrev Minimalist.Merge.SyntacticObjectH : Type

Linglib-specific alias: syntactic objects in the Hopf-algebra layer. M-C-B §1.1.2 + Def 1.2.4 with leaf type LIToken.

Equations

• Minimalist.Merge.SyntacticObjectH = ConnesKreimer.DecoratedTree Minimalist.LIToken

def Minimalist.toHPlanar : FreeMagma (LIToken ⊕ ℕ) → Merge.SyntacticObjectH

Underlying FreeMagma-side embedding from a planar representative into SyntacticObjectH. toH is genuinely planar (DecoratedTree.node distinguishes left from right), so this is representative-dependent. Public so HeadFunction.toHWith can compose it with a chosen externalize section.

Equations

• Minimalist.toHPlanar (FreeMagma.of (Sum.inl tok)) = ConnesKreimer.DecoratedTree.leaf tok
• Minimalist.toHPlanar (FreeMagma.of (Sum.inr val)) = (ConnesKreimer.DecoratedTree.leaf (Minimalist.mkTraceToken 0)).trace
• Minimalist.toHPlanar (l.mul r) = ConnesKreimer.DecoratedTree.node (Minimalist.toHPlanar l) (Minimalist.toHPlanar r)

noncomputable def Minimalist.SyntacticObject.toH (so : SyntacticObject) : Merge.SyntacticObjectH

Embed a plain SyntacticObject into the Hopf-side SyntacticObjectH. Phase 1.0 noncomputable via Quot.out; the parameterized HeadFunction.toHWith takes an explicit externalize for orientation.

Equations

• so.toH = Minimalist.toHPlanar (Quot.out so)

def Minimalist.HeadFunction.toHWith (h : HeadFunction) (so : SyntacticObject) : Merge.SyntacticObjectH

Parameterized embedding: toH under head function h, using h.section_.σ to pick the planar representative. Computable when h.section_.σ is.

Equations

• h.toHWith so = Minimalist.toHPlanar (h.section_.σ so)

def Minimalist.toHcPlanar : FreeMagma (LIToken ⊕ ℕ) → ConnesKreimer.TraceTree LIToken Unit

Underlying FreeMagma-side toHc on a planar representative. Public so HeadFunction.toHcWith can compose it with a chosen externalize.

Equations

• Minimalist.toHcPlanar (FreeMagma.of (Sum.inl tok)) = ConnesKreimer.TraceTree.leaf tok
• Minimalist.toHcPlanar (FreeMagma.of (Sum.inr val)) = ConnesKreimer.TraceTree.trace ()
• Minimalist.toHcPlanar (l.mul r) = (Minimalist.toHcPlanar l).node (Minimalist.toHcPlanar r)

noncomputable def Minimalist.SyntacticObject.toHc (so : SyntacticObject) : ConnesKreimer.TraceTree LIToken Unit

Project a SyntacticObject directly to the bialgebra carrier TraceTree LIToken Unit.

Since SyntacticObject := FreeCommMagma (LIToken ⊕ Nat), this is a planar projection: it picks a representative via Quot.out and serializes left-to-right. Phase 1.0 noncomputable; the parameterized HeadFunction.toHcWith takes an explicit externalize.

Equations

• so.toHc = Minimalist.toHcPlanar (Quot.out so)

def Minimalist.HeadFunction.toHcWith (h : HeadFunction) (so : SyntacticObject) : ConnesKreimer.TraceTree LIToken Unit

Parameterized projection: toHc under head function h, using h.section_.σ to pick the planar representative. Computable when h.section_.σ is.

Equations

• h.toHcWith so = Minimalist.toHcPlanar (h.section_.σ so)

Singleton-class simp lemmas

toHc_leaf / toHc_trace are recoverable as simp lemmas because leaf-only equivalence classes under FreeMagma.CommRel are singletons (no swap constructor fires on .of _). The proof routes through Quot.out_eq + mk_eq_iff_commEqv + the singleton structure of .of.

toHc_mul does NOT recover at this level: (l * r).out may pick either mul l.out r.out or mul r.out l.out, and TraceTree.node is planar (.node a b ≠ .node b a). Phase 2 will take an HeadFunction parameter to canonicalize the orientation.

@[simp]

theorem Minimalist.SyntacticObject.toHc_leaf (tok : LIToken) : (leaf tok).toHc = ConnesKreimer.TraceTree.leaf tok

@[simp]

theorem Minimalist.SyntacticObject.toHc_trace (n : ℕ) : (trace n).toHc = ConnesKreimer.TraceTree.trace ()

Singleton-class simp lemmas for toHcWith/toHWith (parameterized)

All three lemmas reduce via the keystone FreeCommMagma.Section.σ_of helper: the section's image of FreeCommMagma.of x is exactly FreeMagma.of x.

@[simp]

theorem Minimalist.HeadFunction.toHcWith_leaf (h : HeadFunction) (tok : LIToken) : h.toHcWith (SyntacticObject.leaf tok) = ConnesKreimer.TraceTree.leaf tok

toHcWith h on a leaf returns the corresponding TraceTree.leaf.

@[simp]

theorem Minimalist.HeadFunction.toHcWith_trace (h : HeadFunction) (n : ℕ) : h.toHcWith (SyntacticObject.trace n) = ConnesKreimer.TraceTree.trace ()

toHcWith h on a trace returns TraceTree.trace ().

@[simp]

theorem Minimalist.HeadFunction.toHWith_leaf (h : HeadFunction) (tok : LIToken) : h.toHWith (SyntacticObject.leaf tok) = ConnesKreimer.DecoratedTree.leaf tok

toHWith h on a leaf returns the corresponding DecoratedTree.leaf.

theorem Minimalist.isTrace_mkTrace (n : ℕ) : isTrace (mkTrace n) = some n

mkTrace n = .trace n, so isTrace (.trace n) = some n.

theorem Minimalist.mkTrace_toHc (n : ℕ) : (mkTrace n).toHc = ConnesKreimer.TraceTree.trace ()

(mkTrace n).toHc = .trace () — the IM bridge identity.

def Minimalist.Merge.treeToSyntacticObject? : ConnesKreimer.DecoratedTree LIToken → Option SyntacticObject

Forgetful map from SyntacticObjectH = DecoratedTree LIToken back to plain SyntacticObject: returns none if any trace leaf survives, otherwise some the reconstructed trace-free tree. Used by Merge.External / Merge.Internal to bridge the Hopf side to Step.apply (which operates on SyntacticObject).

Plain function rather than dot-notation extension on ConnesKreimer.DecoratedTree (which would mix LIToken-specific Minimalism content into the generic Core namespace). Callers use Minimalist.Merge.treeToSyntacticObject? t qualified.

Equations

• Minimalist.Merge.treeToSyntacticObject? (ConnesKreimer.DecoratedTree.leaf tok) = some (Minimalist.SyntacticObject.leaf tok)
• Minimalist.Merge.treeToSyntacticObject? t.trace = none
• Minimalist.Merge.treeToSyntacticObject? (l.node r) = do let l' ← Minimalist.Merge.treeToSyntacticObject? l let r' ← Minimalist.Merge.treeToSyntacticObject? r pure (l' * r')

theorem Minimalist.Merge.treeToSyntacticObject?_ofSO (so : SyntacticObject) : treeToSyntacticObject? so.toH = some so

Round-trip: embedding a trace-free SO and forgetting the trace structure recovers the original.

The statement as given is FALSE for SOs containing traces: treeToSyntacticObject? returns none on trace leaves by construction (line 173), so the round-trip is undefined whenever so contains a .trace _. The honest reformulation requires a "trace-free" hypothesis (e.g., (traceIndices so).card = 0, importable from TraceInterpretation).

Even with the trace-free hypothesis, the proof requires a representative-level induction through Quot.out-based toH that is more involved than the leaf/trace singleton-class simps. Deferred to Phase 2 alongside head-function parameterization.