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

This file was deleted at commit e0876460 (0.230.913 — "MCB substrate Phase A.5-A.6

• hard delete of legacy CK substrate") and restored on 2026-05-13 because the consumer migration that was supposed to follow the deletion never happened. Merge stack files (Theories/Syntax/Minimalist/Merge/*) and downstream consumers broke on clean build for ~weeks; this restoration unblocks them.

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 α], with consumers migrated to use RootedTree.ConnesKreimer R T + comulCAlgHomP / Planar (α ⊕ β).

Do not extend, do not add new consumers, do not deepen the parallel substrate. The new substrate at Linglib/Core/Algebra/RootedTree/ and Linglib/Core/Combinatorics/RootedTree/ is the canonical destination.

---

Decorated Binary Rooted Trees @cite{marcolli-chomsky-berwick-2025} @cite{foissy-2002}

The decorated binary rooted tree carrier of the Connes-Kreimer-style Hopf algebra of (binary nonplanar) decorated forests, parameterized over a leaf type α : Type*.

Substrate choice

DecoratedTree α is a single inductive with three constructors:

• leaf : α → DecoratedTree α
• trace : DecoratedTree α → DecoratedTree α
• node : DecoratedTree α → DecoratedTree α → DecoratedTree α

Mathematically this is the free term algebra over the signature {leaf : α → 1, trace : 1 → 1, node : 1 × 1 → 1}. The carrier shape is the standard one for decorated Connes-Kreimer Hopf algebras (cf. @cite{foissy-2002} on planar decorated rooted-tree Hopf algebras H^D_{P,R} — generalizing the non-planar Connes-Kreimer H^D_R). Note: M-C-B themselves do not cite Foissy directly; they appeal to the Connes-Kreimer-Feynman-graph proof for coassociativity (book p. 38 references). The Foissy attribution here is the formaliser's reading of the closest mathematical predecessor for the decorated binary case. The Mul (DecoratedTree α) instance (via node) recovers FreeMagma-style * notation; the recursor recOnMul mirrors FreeMagma.recOnMul.

Two faithfulness gaps re. M-C-B Definition 1.1.1

@cite{marcolli-chomsky-berwick-2025} Definition 1.1.1 says the abstract syntactic-object set is a free non-associative commutative magma Magma_{na,c}(SO_0, M). mathlib's FreeMagma α is the non-commutative version. Two distinct gaps relative to mathlib infrastructure:

Gap 1 — Planar vs nonplanar. DecoratedTree α inherits the planar structure: node l r ≠ node r l as an equality. A faithful encoding would Quotient by node l r ~ node r l. Proofs that need the abstract identification require that quotient; this file does not develop it (see CHANGELOG 0.230.655's note on the in-flight FreeCommMagma work). M-C-B handle this gap implicitly via equivalence-class drawings — book p. 23 example shows α∧β∧γ = α∧γ∧β as the same nonplanar tree.

Gap 2 — Set vs multiset (the singleton-collapse). M-C-B p. 25 §1.1.3.1's "very mild" remark refers SPECIFICALLY to the set-vs-multiset clash for syntactic objects: since trees are binary (not n-ary for n ≥ 3), repeated-label ambiguity at a single node is limited, and they explicitly identify {a, a} with {a} for binary nodes. (This is the idem axiom the comm-quotient does NOT add by default.) NOT to be confused with Gap 1 — this is a separate concern.

For workspaces (Forest α := Multiset (DecoratedTree α)), the multiset structure handles the analogous gap at the workspace level automatically. Both gaps remain open at the intra-tree level until the comm-quotient + singleton-collapse are wired in (Stage 4a/4b per scratch/mcb_stage1_plan.md).

Trace constructor and self-reference

Per @cite{marcolli-chomsky-berwick-2025} Definition 1.2.4, the contraction quotient T/^c T_v carries a trace label T_v that holds the contracted subtree as data. The recursive .trace t constructor here is retained for CI-side / FormCopy consumers — operations that need to inspect the original moved subtree at the Conceptual-Intensional interface. Per @cite{marcolli-skigin-2025} §10.1 (which clarifies and disambiguates the brief discussion in M-C-B's §1.3), the recursive payload is not required for the bialgebra structure itself: M-S Lemma 10.4 proves coassociativity of Δ^c with scalar trace labels (see TraceTree α β below). The recursive DecoratedTree α → DecoratedTree α shape is kept here because FormCopy and similar linguistic operations consume the contracted subtree as data; the bialgebra carrier (Hc R α) projects through .anon to a scalar-trace TraceTree α Unit.

Layer status

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

DecoratedTree

inductive ConnesKreimer.DecoratedTree (α : Type u_1) : Type u_1

A binary nonplanar rooted tree with leaves labelled by α and self-decoration via trace. Three constructors:

• leaf a — a leaf vertex labelled with a : α
• trace t — a trace leaf carrying a subtree t as data (treated as a leaf for tree-traversal; t is metadata)
• node l r — a binary internal vertex with children l and r

The trace constructor enables nested decorations (a trace can contain trace-bearing trees), which is essential for iterated coproducts (Δ ⊗ id) ∘ Δ.

• leaf {α : Type u_1} (a : α) : DecoratedTree α
• trace {α : Type u_1} (t : DecoratedTree α) : DecoratedTree α
• node {α : Type u_1} (l r : DecoratedTree α) : DecoratedTree α

@[implicit_reducible]

instance ConnesKreimer.instReprDecoratedTree {α✝ : Type u_1} [Repr α✝] : Repr (DecoratedTree α✝)

Equations

• ConnesKreimer.instReprDecoratedTree = { reprPrec := ConnesKreimer.instReprDecoratedTree.repr }

def ConnesKreimer.instReprDecoratedTree.repr {α✝ : Type u_1} [Repr α✝] : DecoratedTree α✝ → ℕ → Std.Format

Equations

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

def ConnesKreimer.instDecidableEqDecoratedTree.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : DecoratedTree α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.instDecidableEqDecoratedTree.decEq (ConnesKreimer.DecoratedTree.leaf a) (ConnesKreimer.DecoratedTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq (ConnesKreimer.DecoratedTree.leaf a) t.trace = isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq (ConnesKreimer.DecoratedTree.leaf a) (l.node r) = isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq t.trace (ConnesKreimer.DecoratedTree.leaf a) = isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq a.trace b.trace = if h : a = b then h ▸ have inst := ConnesKreimer.instDecidableEqDecoratedTree.decEq a a; isTrue ⋯ else isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq t.trace (l.node r) = isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq (l.node r) (ConnesKreimer.DecoratedTree.leaf a) = isFalse ⋯
• ConnesKreimer.instDecidableEqDecoratedTree.decEq (l.node r) t.trace = isFalse ⋯

@[implicit_reducible]

instance ConnesKreimer.instDecidableEqDecoratedTree {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (DecoratedTree α✝)

Equations

• ConnesKreimer.instDecidableEqDecoratedTree = ConnesKreimer.instDecidableEqDecoratedTree.decEq

Mathlib-style algebra hooks

@[implicit_reducible]

instance ConnesKreimer.DecoratedTree.instMul {α : Type u_1} : Mul (DecoratedTree α)

DecoratedTree α is a magma via the node constructor, mirroring FreeMagma. This gives l * r = .node l r for free.

Equations

• ConnesKreimer.DecoratedTree.instMul = { mul := ConnesKreimer.DecoratedTree.node }

@[simp]

theorem ConnesKreimer.DecoratedTree.node_eq_mul {α : Type u_1} (l r : DecoratedTree α) : l.node r = l * r

node l r = l * r by definition.

def ConnesKreimer.DecoratedTree.recOnMul {α : Type u_1} {motive : DecoratedTree α → Sort u_2} (t : DecoratedTree α) (leaf : (a : α) → motive (leaf a)) (trace : (s : DecoratedTree α) → motive s → motive s.trace) (mul : (a b : DecoratedTree α) → motive a → motive b → motive (a * b)) : motive t

Recursor using * notation in the node/mul case, mirroring FreeMagma.recOnMul. Useful for proofs and definitions that prefer the multiplicative interface.

Equations

• ConnesKreimer.DecoratedTree.recOnMul (ConnesKreimer.DecoratedTree.leaf a) leaf trace mul = leaf a
• ConnesKreimer.DecoratedTree.recOnMul a.trace leaf trace mul = trace a (ConnesKreimer.DecoratedTree.recOnMul a leaf trace mul)
• ConnesKreimer.DecoratedTree.recOnMul (a.node a_1) leaf trace mul = mul a a_1 (ConnesKreimer.DecoratedTree.recOnMul a leaf trace mul) (ConnesKreimer.DecoratedTree.recOnMul a_1 leaf trace mul)

def ConnesKreimer.DecoratedTree.leafCount {α : Type u_1} : DecoratedTree α → ℕ

Number of leaves in a DecoratedTree. Both .leaf and .trace count as leaves (each occupies one leaf vertex in the tree shape; the contracted subtree carried by .trace is metadata, not part of the visible tree).

Equations

• (ConnesKreimer.DecoratedTree.leaf a).leafCount = 1
• a.trace.leafCount = 1
• (a.node a_1).leafCount = a.leafCount + a_1.leafCount

@[simp]

theorem ConnesKreimer.DecoratedTree.leafCount_leaf {α : Type u_1} (a : α) : (leaf a).leafCount = 1

@[simp]

theorem ConnesKreimer.DecoratedTree.leafCount_trace {α : Type u_1} (t : DecoratedTree α) : t.trace.leafCount = 1

@[simp]

theorem ConnesKreimer.DecoratedTree.leafCount_node {α : Type u_1} (l r : DecoratedTree α) : (l.node r).leafCount = l.leafCount + r.leafCount

theorem ConnesKreimer.DecoratedTree.leafCount_pos {α : Type u_1} (t : DecoratedTree α) : 0 < t.leafCount

IsNotTrace predicate

For Connes-Kreimer coassociativity to hold (M-C-B Lemma 1.2.10), cuts that extract a child subtree (bothCut, onlyLeftCut, onlyRightCut on .node) must NOT be allowed when the relevant child is a .trace marker. Without this restriction, iterated cuts on the remainder accumulate .trace (.trace _) nesting, breaking the cuts-of-cuts bijection — see scratch/mcb_stage1_plan.md or Linglib/Scratch/CoassocCheck.lean for the full analysis.

IsNotTrace t : Prop is True for .leaf and .node, False for .trace. Decidable; used as a hypothesis in CutShape's extracting constructors.

def ConnesKreimer.DecoratedTree.IsNotTrace {α : Type u_1} : DecoratedTree α → Prop

A tree is "not a trace marker" — required for cuts that extract this tree as a subtree. Predicate is decidable.

Equations

• (ConnesKreimer.DecoratedTree.leaf a).IsNotTrace = True
• a.trace.IsNotTrace = False
• (a.node a_1).IsNotTrace = True

@[implicit_reducible]

instance ConnesKreimer.DecoratedTree.instDecidablePredIsNotTrace {α : Type u_1} : DecidablePred IsNotTrace

Equations

• (ConnesKreimer.DecoratedTree.leaf a).instDecidablePredIsNotTrace = isTrue trivial
• a.trace.instDecidablePredIsNotTrace = isFalse ⋯
• (a.node a_1).instDecidablePredIsNotTrace = isTrue trivial

@[simp]

theorem ConnesKreimer.DecoratedTree.isNotTrace_leaf {α : Type u_1} (a : α) : (leaf a).IsNotTrace

@[simp]

theorem ConnesKreimer.DecoratedTree.isNotTrace_node {α : Type u_1} (l r : DecoratedTree α) : (l.node r).IsNotTrace

@[simp]

theorem ConnesKreimer.DecoratedTree.not_isNotTrace_trace {α : Type u_1} (t : DecoratedTree α) : ¬t.trace.IsNotTrace

TraceTree — trace label as a first-class scalar

The .trace t constructor of DecoratedTree α carries the contracted subtree t as metadata, motivated by the linguistic FormCopy operation (@cite{marcolli-chomsky-berwick-2025} Definition 1.2.4). However, the Hopf algebra coassociativity proof in the M-C-B book Lemma 1.2.10 appeals to @cite{connes-kreimer-1998} for the Feynman-graph CK Hopf algebra, where contraction markers carry no recursive payload. Treating .trace t literally as a data-carrying basis element of Hc R α would break coassociativity: iterated coproducts produce .trace _ markers whose contents differ between the two iteration orders, even though the underlying combinatorial "3-coloring" structures match. (A concrete counterexample for T = .node l (.node a b) is verified kernel-checked in scratch/SlotThreeMismatch.lean.)

@cite{marcolli-skigin-2025} §10.1 ("Labels of traces of movement") explicitly addresses this. M-S frame their §10 as clarifying and disambiguating M-C-B's §1.3, observing: the trace label "in fact does not have to retain the full structure of T_v as a syntactic object … the extracted term T_v is still present, on the other side of the coproduct, so that information is not lost." Their Definition 10.3 redefines the trace label as a scalar α̅_{h_T(v)} — the struck-through head label, an element of ̄SO₀ := {̄α | α ∈ SO₀} (a disjoint marked copy of the leaf alphabet, NOT just an element of SO₀). The leaf alphabet is enlarged to the disjoint union SO₀ ⊔ ̄SO₀. M-S Lemma 10.4 proves Δ^c coassociativity under this scheme via head-function transparency: h_{T_v}(w) = h_T(w) for w ∈ T_v, so iterated traces all resolve to the same label as the original subtree.

TraceTree α β realizes the disjoint-leaf-and-trace shape with a polymorphic trace-label type β:

• .leaf (a : α): a leaf carrying a label of type α.
• .trace (b : β): a trace marker carrying a scalar label of type β (NOT a recursive subtree). The constructor distinction encodes the disjoint-copy structure of SO₀ ⊔ ̄SO₀: even when β = α, the .trace-vs-.leaf distinction marks the struck-through copy.
• .node l r: an internal binary vertex.

Hc R α is fixed to Multiset (TraceTree α Unit) — the simplest realization, where trace labels carry no information at all. This is sufficient for coassociativity (M-S Lemma 10.4 holds vacuously when the extractor is constant) but is a strict simplification of M-S, who use a non-trivial scalar label via the head function. The polymorphism stays available so linguistic-layer code can use TraceTree α α (M-S aligned) or richer label types when head-function infrastructure lands.

The projection DecoratedTree.anon (h : DecoratedTree α → β) takes an extractor function for the trace label. For Hc-level coassoc to behave, h must be transparent under contraction: h (.trace t) = h t. This is an explicit hypothesis on theorems that need it (mathlib idiom: unbundled function plus side-condition, since trace-label choice is not canonical). Examples of transparent extractors:

• fun _ => () (trivial) — used by Hc R α itself.
• DecoratedTree.leftmostLeaf (when defined) — recursive descent through .trace, picking the leftmost actual leaf label.
• The M-S head function (when head-function infrastructure lands).

The labelled .trace t data remains available at the DecoratedTree level for linguistic operations (FormCopy, cancellation-of-deeper-copies).

inductive ConnesKreimer.TraceTree (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

A binary rooted tree with leaf labels in α and scalar trace labels in β. Used as the basis-key type of Hc R α (with β = Unit). The polymorphic β accommodates richer linguistic-layer projections (e.g., β = α plus a head function realizes @cite{marcolli-skigin-2025} Definition 10.3, modulo the head-function-transparency requirement on the extractor).

• leaf {α : Type u_1} {β : Type u_2} (a : α) : TraceTree α β
• trace {α : Type u_1} {β : Type u_2} (b : β) : TraceTree α β
• node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : TraceTree α β

@[implicit_reducible]

instance ConnesKreimer.instReprTraceTree {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Repr (TraceTree α✝ β✝)

Equations

• ConnesKreimer.instReprTraceTree = { reprPrec := ConnesKreimer.instReprTraceTree.repr }

def ConnesKreimer.instReprTraceTree.repr {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : TraceTree α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConnesKreimer.instDecidableEqTraceTree {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (TraceTree α✝ β✝)

Equations

• ConnesKreimer.instDecidableEqTraceTree = ConnesKreimer.instDecidableEqTraceTree.decEq

def ConnesKreimer.instDecidableEqTraceTree.decEq {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : TraceTree α✝ β✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.leaf a) (ConnesKreimer.TraceTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.leaf a) (ConnesKreimer.TraceTree.trace b) = isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.leaf a) (l.node r) = isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.trace b) (ConnesKreimer.TraceTree.leaf a) = isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.trace a) (ConnesKreimer.TraceTree.trace b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (ConnesKreimer.TraceTree.trace b) (l.node r) = isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (l.node r) (ConnesKreimer.TraceTree.leaf a) = isFalse ⋯
• ConnesKreimer.instDecidableEqTraceTree.decEq (l.node r) (ConnesKreimer.TraceTree.trace b) = isFalse ⋯

def ConnesKreimer.TraceTree.IsNotTrace {α : Type u_1} {β : Type u_2} : TraceTree α β → Prop

A TraceTree is "not a trace marker" — required for cuts that extract this tree as a subtree. Predicate is decidable. Same shape as DecoratedTree.IsNotTrace.

Equations

• (ConnesKreimer.TraceTree.leaf a).IsNotTrace = True
• (ConnesKreimer.TraceTree.trace a).IsNotTrace = False
• (a.node a_1).IsNotTrace = True

@[implicit_reducible]

instance ConnesKreimer.TraceTree.instDecidablePredIsNotTrace {α : Type u_1} {β : Type u_2} : DecidablePred IsNotTrace

Equations

• (ConnesKreimer.TraceTree.leaf a).instDecidablePredIsNotTrace = isTrue trivial
• (ConnesKreimer.TraceTree.trace a).instDecidablePredIsNotTrace = isFalse ⋯
• (a.node a_1).instDecidablePredIsNotTrace = isTrue trivial

@[simp]

theorem ConnesKreimer.TraceTree.isNotTrace_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).IsNotTrace

@[simp]

theorem ConnesKreimer.TraceTree.isNotTrace_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).IsNotTrace

@[simp]

theorem ConnesKreimer.TraceTree.not_isNotTrace_trace {α : Type u_1} {β : Type u_2} (b : β) : ¬(trace b).IsNotTrace

def ConnesKreimer.TraceTree.size {α : Type u_1} {β : Type u_2} : TraceTree α β → ℕ

Size measure on TraceTree: count of constructors (each .leaf / .trace / .node adds 1). Used as the structural-recursion measure for proving cutForest extracts proper subtrees.

Equations

• (ConnesKreimer.TraceTree.leaf a).size = 1
• (ConnesKreimer.TraceTree.trace a).size = 1
• (a.node a_1).size = 1 + a.size + a_1.size

@[simp]

theorem ConnesKreimer.TraceTree.size_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).size = 1

@[simp]

theorem ConnesKreimer.TraceTree.size_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).size = 1

@[simp]

theorem ConnesKreimer.TraceTree.size_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).size = 1 + l.size + r.size

theorem ConnesKreimer.TraceTree.size_pos {α : Type u_1} {β : Type u_2} (t : TraceTree α β) : 0 < t.size

def ConnesKreimer.TraceTree.nonTraceSize {α : Type u_1} {β : Type u_2} : TraceTree α β → ℕ

Vertex count excluding .trace markers. The trace-aware analog of size. Used by Δ^c counting because per @cite{marcolli-chomsky-berwick-2025} Lemma 1.6.3 eq. 1.6.8 (book p. 65), trace markers in T/^c T_v are NOT counted as accessible terms ("cancellation of the deeper copy").

Equations

• (ConnesKreimer.TraceTree.leaf a).nonTraceSize = 1
• (ConnesKreimer.TraceTree.trace a).nonTraceSize = 0
• (a.node a_1).nonTraceSize = 1 + a.nonTraceSize + a_1.nonTraceSize

@[simp]

theorem ConnesKreimer.TraceTree.nonTraceSize_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).nonTraceSize = 1

@[simp]

theorem ConnesKreimer.TraceTree.nonTraceSize_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).nonTraceSize = 0

@[simp]

theorem ConnesKreimer.TraceTree.nonTraceSize_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).nonTraceSize = 1 + l.nonTraceSize + r.nonTraceSize

theorem ConnesKreimer.TraceTree.nonTraceSize_le_size {α : Type u_1} {β : Type u_2} (t : TraceTree α β) : t.nonTraceSize ≤ t.size

def ConnesKreimer.TraceTree.leafCount {α : Type u_1} {β : Type u_2} : TraceTree α β → ℕ

Leaf count of a TraceTree. The Hopf-algebra grading on Hc R α = AddMonoidAlgebra R (TraceForest α Unit) per @cite{marcolli-chomsky-berwick-2025} Definition 1.6.2 (book p. 64): deg(a) = #L(T_a). Both .leaf and .trace count as 1 (a trace marker occupies a leaf position in the tree); .node l r sums children. Same shape as DecoratedTree.leafCount.

Equations

• (ConnesKreimer.TraceTree.leaf a).leafCount = 1
• (ConnesKreimer.TraceTree.trace a).leafCount = 1
• (a.node a_1).leafCount = a.leafCount + a_1.leafCount

@[simp]

theorem ConnesKreimer.TraceTree.leafCount_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).leafCount = 1

@[simp]

theorem ConnesKreimer.TraceTree.leafCount_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).leafCount = 1

@[simp]

theorem ConnesKreimer.TraceTree.leafCount_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).leafCount = l.leafCount + r.leafCount

theorem ConnesKreimer.TraceTree.leafCount_pos {α : Type u_1} {β : Type u_2} (t : TraceTree α β) : 0 < t.leafCount

Migration bridge to FreeCommMagma

The planar TraceTree α β is being migrated to the nonplanar FreeCommMagma (α ⊕ β) per the M-C-B (2025) Definition 1.1.1 "free, non-associative, commutative magma" identification of syntactic objects (book p. 22, Remark 1.1.2). Linguistically-essential operations like phonological yield and head projection move to a separate Linearization theory; the TraceTree carrier becomes a "chosen planar embedding" rather than the primary representation.

The coercion below is a one-way bridge (planar → nonplanar): TraceTree.toFreeCommMagma forgets the left/right child order at each .node, mapping it onto the unordered FreeCommMagma.mul. The reverse direction requires a linearization choice (Phase 2 of the migration) and is not single-valued.

def ConnesKreimer.TraceTree.toFreeCommMagma {α : Type u_1} {β : Type u_2} : TraceTree α β → FreeCommMagma (α ⊕ β)

Migration bridge: forget the planar order. Maps TraceTree α β into FreeCommMagma (α ⊕ β) by sending .leaf a to of (.inl a), .trace b to of (.inr b), and .node l r to `l.toFreeCommMagma

• r.toFreeCommMagma` (multiplication is commutative on the target, so the planar choice is forgotten).

This is a one-way coercion intended for the migration window: the nonplanar carrier is the canonical M-C-B-aligned representation; the planar TraceTree survives only as a chosen planar embedding consumed by Linearization.

Equations

• (ConnesKreimer.TraceTree.leaf a).toFreeCommMagma = FreeCommMagma.of (Sum.inl a)
• (ConnesKreimer.TraceTree.trace a).toFreeCommMagma = FreeCommMagma.of (Sum.inr a)
• (a.node a_1).toFreeCommMagma = a.toFreeCommMagma * a_1.toFreeCommMagma

@[simp]

theorem ConnesKreimer.TraceTree.toFreeCommMagma_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).toFreeCommMagma = FreeCommMagma.of (Sum.inl a)

@[simp]

theorem ConnesKreimer.TraceTree.toFreeCommMagma_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).toFreeCommMagma = FreeCommMagma.of (Sum.inr b)

@[simp]

theorem ConnesKreimer.TraceTree.toFreeCommMagma_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).toFreeCommMagma = l.toFreeCommMagma * r.toFreeCommMagma

theorem ConnesKreimer.TraceTree.toFreeCommMagma_swap {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).toFreeCommMagma = (r.node l).toFreeCommMagma

Sanity: planar swap collapses under toFreeCommMagma. The two distinct planar trees .node l r and .node r l map to the same FreeCommMagma element (the witness that the bridge is "forgetful" in the right way).

def ConnesKreimer.DecoratedTree.anon {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) : DecoratedTree α → TraceTree α β

Project a DecoratedTree α to a TraceTree α β, computing each trace's label via the extractor h. Recurses through .node; applies h once at each .trace.

For Hc-level coassoc (forestToHc-respecting equality of iterated coproducts), h must satisfy the transparency condition ∀ t, h (.trace t) = h t so that nested traces resolve to the same label as the original subtree. The condition is stated as an explicit hypothesis on theorems that need it.

Equations

• ConnesKreimer.DecoratedTree.anon h (ConnesKreimer.DecoratedTree.leaf a) = ConnesKreimer.TraceTree.leaf a
• ConnesKreimer.DecoratedTree.anon h a.trace = ConnesKreimer.TraceTree.trace (h a)
• ConnesKreimer.DecoratedTree.anon h (a.node a_1) = (ConnesKreimer.DecoratedTree.anon h a).node (ConnesKreimer.DecoratedTree.anon h a_1)

@[simp]

theorem ConnesKreimer.DecoratedTree.anon_leaf {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (a : α) : anon h (leaf a) = TraceTree.leaf a

@[simp]

theorem ConnesKreimer.DecoratedTree.anon_trace {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (t : DecoratedTree α) : anon h t.trace = TraceTree.trace (h t)

@[simp]

theorem ConnesKreimer.DecoratedTree.anon_node {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (l r : DecoratedTree α) : anon h (l.node r) = (anon h l).node (anon h r)

Forest

A forest is a multiset of decorated trees. Disjoint union ⊔ corresponds to · + · on multisets (commutative, ∅ = 0). @cite{marcolli-chomsky-berwick-2025} Definition 1.2.1.

@[reducible, inline]

abbrev ConnesKreimer.Forest (α : Type u_1) : Type u_1

A decorated forest: a multiset of decorated trees.

Equations

• ConnesKreimer.Forest α = Multiset (ConnesKreimer.DecoratedTree α)

@[reducible, inline]

abbrev ConnesKreimer.TraceForest (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

A forest of TraceTrees with leaf labels in α and trace labels in β. Used as the basis-key type of Hc R α (with β = Unit).

Equations

• ConnesKreimer.TraceForest α β = Multiset (ConnesKreimer.TraceTree α β)

def ConnesKreimer.TraceForest.degForest {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

The total leaf count of a TraceForest: sum of TraceTree.leafCount over its components. The Hopf-algebra grading on Hc R α per @cite{marcolli-chomsky-berwick-2025} Definition 1.6.2 (book p. 64): deg(F) = #L(F). M-C-B's degree-conservation observation (book p. 64, paragraph after Def 1.6.2): deg(F) is conserved across any Merge operation since no lexical items are removed.

Equations

• F.degForest = (Multiset.map ConnesKreimer.TraceTree.leafCount F).sum

@[simp]

theorem ConnesKreimer.TraceForest.degForest_zero {α : Type u_1} {β : Type u_2} : degForest 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.degForest_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.degForest = T.leafCount

@[simp]

theorem ConnesKreimer.TraceForest.degForest_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).degForest = F.degForest + G.degForest

@[simp]

theorem ConnesKreimer.TraceForest.degForest_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : degForest (T ::ₘ F) = T.leafCount + F.degForest

@[simp]

theorem ConnesKreimer.TraceForest.degForest_pair {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : {l, r}.degForest = l.leafCount + r.leafCount

Pair forest: degForest {l, r} = l.leafCount + r.leafCount. Avoids repeating the ({l, r} : Multiset _) = l ::ₘ {r} rewrite + _cons + _singleton chain at each call site (notably in AdmissibleCut.cut_leafCount_conservation's bothCut arm).

def ConnesKreimer.TraceForest.sizeForest {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

Total vertex count of a TraceForest: sum of TraceTree.size over its components. Vertex-count analog of degForest (which sums leafCount). Used by cut_size_conservation (in AdmissibleCut.lean) to express the Δ^d size analog of MCB's leafCount-conservation observation.

Equations

• F.sizeForest = (Multiset.map ConnesKreimer.TraceTree.size F).sum

@[simp]

theorem ConnesKreimer.TraceForest.sizeForest_zero {α : Type u_1} {β : Type u_2} : sizeForest 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.sizeForest_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.sizeForest = T.size

@[simp]

theorem ConnesKreimer.TraceForest.sizeForest_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : sizeForest (T ::ₘ F) = T.size + F.sizeForest

@[simp]

theorem ConnesKreimer.TraceForest.sizeForest_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).sizeForest = F.sizeForest + G.sizeForest

@[simp]

theorem ConnesKreimer.TraceForest.sizeForest_pair {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : {l, r}.sizeForest = l.size + r.size

def ConnesKreimer.Forest.anon {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (F : Forest α) : TraceForest α β

Project a forest to a TraceForest α β via the per-tree anon h map.

Defined as prefix Forest.anon h F rather than dot-notation F.anon, because Forest is an abbrev for Multiset (DecoratedTree α) and dot-notation on abbrevs routes to the underlying type's namespace.

Equations

• ConnesKreimer.Forest.anon h F = Multiset.map (ConnesKreimer.DecoratedTree.anon h) F

@[simp]

theorem ConnesKreimer.Forest.anon_zero {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) : anon h 0 = 0

@[simp]

theorem ConnesKreimer.Forest.anon_add {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (F G : Forest α) : anon h (F + G) = anon h F + anon h G

@[simp]

theorem ConnesKreimer.Forest.anon_singleton {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (T : DecoratedTree α) : anon h {T} = {DecoratedTree.anon h T}

@[simp]

theorem ConnesKreimer.Forest.anon_cons {α : Type u_1} {β : Type u_2} (h : DecoratedTree α → β) (T : DecoratedTree α) (F : Forest α) : anon h (T ::ₘ F) = DecoratedTree.anon h T ::ₘ anon h F

§6: Forest size measures (b₀, α, σ)

@cite{marcolli-chomsky-berwick-2025} §1.2 + §1.6.1

Three counting functions on a TraceForest α β, parallel to degForest and sizeForest above:

• b₀(F) — number of components: cardinality of F as a multiset.
• α(F) — accessible terms: per MCB Def 1.2.2 (the "more precise discussion" of the §1.1 prose-definition on book p. 21: "the accessible terms of a syntactic object T are the subtrees T_v, with v a non-root vertex of T"), α(F) = Σ_T #Acc(T). For a TraceTree, every vertex is the root of some subtree, so #Acc(T) = #V(T) - 1 = T.size - 1.
• σ(F) = b₀(F) + α(F) (MCB §1.6.1).

Lemma 1.6.3 (book §1.6.2) supplies counting identities for these under merge (the .node constructor); the merge-side identities matching MCB eq. 1.6.5 / 1.6.6 are proven below. The cut-quotient identities (eq. 1.6.7- 1.6.10) need substrate from AdmissibleCut.lean and live in Theories/Syntax/Minimalist/Merge/MinimalYield.lean.

Generic over leaf alphabet α and trace alphabet β.

def ConnesKreimer.TraceTree.accCount {α : Type u_1} {β : Type u_2} : TraceTree α β → ℕ

Number of accessible terms of a tree: #V(T) - 1 per MCB Def 1.2.2, where accessible terms are subtrees T_v with v a non-root vertex of T (book p. 21).

Equations

• T.accCount = T.size - 1

@[simp]

theorem ConnesKreimer.TraceTree.accCount_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).accCount = 0

@[simp]

theorem ConnesKreimer.TraceTree.accCount_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).accCount = 0

@[simp]

theorem ConnesKreimer.TraceTree.accCount_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).accCount = l.size + r.size

theorem ConnesKreimer.TraceTree.accCount_merge {α : Type u_1} {β : Type u_2} (T_v T_w : TraceTree α β) : (T_v.node T_w).accCount = T_v.accCount + T_w.accCount + 2

MCB Lemma 1.6.3 eq. 1.6.5 (book p. 65): α(M(T_v, T_w)) = α(T_v) + α(T_w) + 2. Trivially follows from accCount_node plus size_pos.

def ConnesKreimer.TraceForest.b₀ {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

b₀(F) — number of components. M-C-B Definition 1.2.2.

Equations

• F.b₀ = Multiset.card F

@[simp]

theorem ConnesKreimer.TraceForest.b₀_zero {α : Type u_1} {β : Type u_2} : b₀ 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.b₀_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.b₀ = 1

@[simp]

theorem ConnesKreimer.TraceForest.b₀_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : b₀ (T ::ₘ F) = 1 + F.b₀

@[simp]

theorem ConnesKreimer.TraceForest.b₀_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).b₀ = F.b₀ + G.b₀

def ConnesKreimer.TraceForest.alpha {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

α(F) — total accessible terms across components. M-C-B Def 1.2.2 / §1.6.1.

Equations

• F.alpha = (Multiset.map ConnesKreimer.TraceTree.accCount F).sum

@[simp]

theorem ConnesKreimer.TraceForest.alpha_zero {α : Type u_1} {β : Type u_2} : alpha 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.alpha_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.alpha = T.accCount

@[simp]

theorem ConnesKreimer.TraceForest.alpha_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : alpha (T ::ₘ F) = T.accCount + F.alpha

@[simp]

theorem ConnesKreimer.TraceForest.alpha_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).alpha = F.alpha + G.alpha

def ConnesKreimer.TraceForest.sigma {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

σ(F) = b₀(F) + α(F) — total accessible-terms-of-forest measure (MCB §1.6.1 eq. 1.6.1).

Equations

• F.sigma = F.b₀ + F.alpha

@[simp]

theorem ConnesKreimer.TraceForest.sigma_zero {α : Type u_1} {β : Type u_2} : sigma 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.sigma_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.sigma = 1 + T.accCount

@[simp]

theorem ConnesKreimer.TraceForest.sigma_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : sigma (T ::ₘ F) = 1 + T.accCount + F.sigma

@[simp]

theorem ConnesKreimer.TraceForest.sigma_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).sigma = F.sigma + G.sigma

theorem ConnesKreimer.TraceForest.sigma_merge_singleton {α : Type u_1} {β : Type u_2} (T_v T_w : TraceTree α β) : {T_v.node T_w}.sigma = {T_v}.sigma + {T_w}.sigma + 1

MCB Lemma 1.6.3 eq. 1.6.6 (book p. 65): σ(M(T_v, T_w)) = σ(T_v) + σ(T_w) + 1 at the singleton-forest level.

§7: Δ^c-aware forest measures (αᶜ, σᶜ)

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

Trace-aware analogs of accCount and sigma for the Δ^c counting (MCB Lemma 1.6.3 eq. 1.6.8 and 1.6.10). These count trace markers as zero contribution to "accessible terms" — implementing MCB's "cancellation of the deeper copy" principle (book p. 65-66). For trace-free trees, accCountC = accCount; the difference shows up only in contraction- quotient trees.

Distinction from accCount:

• accCount T = T.size - 1 (every non-root vertex counted)
• accCountC T = T.nonTraceSize - 1 (only non-trace non-root vertices)

For trace-free trees nonTraceSize = size, so accCountC = accCount. The two measures diverge on T/^c T_v (a trace marker for the cancelled copy), which is exactly where MCB's eq. 1.6.8/1.6.10 use them.

def ConnesKreimer.TraceTree.accCountC {α : Type u_1} {β : Type u_2} : TraceTree α β → ℕ

Δ^c-aware accCount: non-root non-trace vertex count. Excludes trace markers per MCB Lemma 1.6.3 eq. 1.6.8 (book p. 65). For trace-free trees agrees with accCount.

Equations

• T.accCountC = T.nonTraceSize - 1

@[simp]

theorem ConnesKreimer.TraceTree.accCountC_leaf {α : Type u_1} {β : Type u_2} (a : α) : (leaf a).accCountC = 0

@[simp]

theorem ConnesKreimer.TraceTree.accCountC_trace {α : Type u_1} {β : Type u_2} (b : β) : (trace b).accCountC = 0

@[simp]

theorem ConnesKreimer.TraceTree.accCountC_node {α : Type u_1} {β : Type u_2} (l r : TraceTree α β) : (l.node r).accCountC = l.nonTraceSize + r.nonTraceSize

def ConnesKreimer.TraceForest.alphaC {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

αᶜ on a forest. Non-trace non-root vertex count summed across components.

Equations

• F.alphaC = (Multiset.map ConnesKreimer.TraceTree.accCountC F).sum

@[simp]

theorem ConnesKreimer.TraceForest.alphaC_zero {α : Type u_1} {β : Type u_2} : alphaC 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.alphaC_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.alphaC = T.accCountC

@[simp]

theorem ConnesKreimer.TraceForest.alphaC_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : alphaC (T ::ₘ F) = T.accCountC + F.alphaC

@[simp]

theorem ConnesKreimer.TraceForest.alphaC_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).alphaC = F.alphaC + G.alphaC

def ConnesKreimer.TraceForest.sigmaC {α : Type u_1} {β : Type u_2} (F : TraceForest α β) : ℕ

σᶜ on a forest: σᶜ(F) = b₀(F) + αᶜ(F). Δ^c analog of sigma.

Equations

• F.sigmaC = F.b₀ + F.alphaC

@[simp]

theorem ConnesKreimer.TraceForest.sigmaC_zero {α : Type u_1} {β : Type u_2} : sigmaC 0 = 0

@[simp]

theorem ConnesKreimer.TraceForest.sigmaC_singleton {α : Type u_1} {β : Type u_2} (T : TraceTree α β) : {T}.sigmaC = 1 + T.accCountC

@[simp]

theorem ConnesKreimer.TraceForest.sigmaC_cons {α : Type u_1} {β : Type u_2} (T : TraceTree α β) (F : TraceForest α β) : sigmaC (T ::ₘ F) = 1 + T.accCountC + F.sigmaC

@[simp]

theorem ConnesKreimer.TraceForest.sigmaC_add {α : Type u_1} {β : Type u_2} (F G : TraceForest α β) : (F + G).sigmaC = F.sigmaC + G.sigmaC