Δ^c (trace-aware admissible-cut) coproduct on RootedTree.Planar (α ⊕ β) #
@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}
The trace-preserving variant of the Connes-Kreimer admissible-cut
coproduct on planar n-ary rooted trees, parameterized by a trace
encoder τ : Planar (α ⊕ β) → β. For a tree T:
Δ^c_τ(T) = T ⊗ 1 + Σ_{c : Cut T} of'(cutForest c) ⊗ ofTree(remainderTrace c)
where remainderTrace c keeps a placeholder leaf at every cut site —
the leaf's label is Sum.inr (τ T_v) for the cut subtree T_v. This
contrasts with the deletion variant Δ^ρ (sibling Coproduct.lean),
where cut sites simply disappear (the parent loses a child).
Carrier and encoder #
The carrier is Planar (α ⊕ β) directly: original-decoration vertices
sit on Sum.inl, trace-marker vertices on Sum.inr. Output trees from
Δ^c only ever introduce trace markers as leaves; this is provable as a
property rather than baked into the carrier (no DecoratedTree wrapper).
The trace encoder τ is an explicit per-definition parameter, not a
section variable. Consumers pick τ to encode whatever trace
information they want about the cut subtree:
- Unit trace:
β = Unit,τ = Function.const _ ()— placeholder is a single Unit-labeled leaf, identical for every cut. Distinct from MCB's Δ^d (Definition 1.2.5, p. 31), which is deletion-then-rebinarize and would require separate substrate. - Identity trace:
τ = idif β = Planar (α ⊕ β) — placeholder carries the full cut subtree as label. Closest match to the book's notationF̄_v. - Quotient trace:
τprojects to syntactic features, semantic representations, etc. (consumer-specific).
Embedding α-only trees #
The substrate is encoder-free: an α-only tree T : Planar α is embedded
into Planar (α ⊕ β) via Planar.map Sum.inl T. No separate
mapDecoration primitive.
MCB anchors #
- Definition 1.2.4 (book p. 30): T/^c F_v — contraction of each cut subtree to its root vertex, which becomes a leaf carrying a trace label F̄_v. Parent arity preserved.
- Definition 1.2.8 (book p. 33), formula (1.2.8) with ω = c: the
coproduct itself, Δ^c(T) := T ⊗ 1 + 1 ⊗ T + Σ F_v ⊗ T/^c F_v. The
1 ⊗ Tterm is absorbed into the sum here as the empty-cut summand (matchingCoproduct.lean's convention; theT ⊗ 1term is kept explicit). - Remark 1.2.9 (book p. 34): on nonplanar binary rooted trees, Δ^c is the restriction of the coproduct of the Connes-Kreimer Hopf algebra of Feynman graphs.
- Lemma 1.2.10 (book p. 35): coassociativity of Δ^c (proved at the Nonplanar layer; not in this file).
The trace-leaf contraction underlies the C-I (semantic) interface for
FormCopy in the MCB analysis. For the admissible-cut variant Δ^ρ
(corresponds to MCB's Δ^ρ; cut sites removed entirely; result lives
in at-most-n-ary trees), see Coproduct.lean.
Architecture #
The cut enumeration is delegated to CoproductGeneric.lean's
cutSummandsG (extract), parameterized by an extraction policy. Δ^c
specializes via the extraction policy extractC τ:
- For
Sum.inl-rooted (non-trace) subtrees: extract whole, leaving[traceLeaf (τ t)]as a single replacement leaf. - For
Sum.inr-rooted (trace) subtrees: do not extract. Required for coassoc (without this restriction, iterated Δ^c produces "trace of trace" right-channel terms that break the bijection); also matches MCB Definition 1.2.2's restriction of cuts to "accessible terms" at internal non-root vertices, which excludes trace placeholders.
Status #
[UPSTREAM] candidate; future home something like
Mathlib.Combinatorics.RootedTree.CoproductDecorated. Sorry-free.
The trace-marker placeholder leaf carrying the encoded label b : β.
Equations
- RootedTree.ConnesKreimer.traceLeaf b = RootedTree.Planar.node (Sum.inr b) []
Instances For
Δ^c extraction policy #
The Δ^c extraction policy: for Sum.inl-rooted (non-trace)
subtrees, extract whole leaving a single traceLeaf (τ t) in the
parent's child slot. For Sum.inr-rooted (trace) subtrees, decline
to extract.
Equations
- RootedTree.ConnesKreimer.extractC τ (RootedTree.Planar.node (Sum.inl val) cs) = some [RootedTree.ConnesKreimer.traceLeaf (τ (RootedTree.Planar.node (Sum.inl val) cs))]
- RootedTree.ConnesKreimer.extractC τ (RootedTree.Planar.node (Sum.inr val) cs) = none
Instances For
cutSummandsCP — Δ^c cut enumeration via the generic cutSummandsG #
Defined as cutSummandsG (extractC τ). The generic-side simp lemmas
(cutSummandsG_node, cutListSummandsG_*, augActionG_*) compose with
extractC_inl/extractC_inr to give the Δ^c-specific reductions.
The Δ^c cut summands: cuts at non-trace subtrees with trace placeholders, skipping cuts at trace leaves.
Equations
Instances For
comulCTreePlanar — tree-level Δ^c #
Sum the cut summands as tensors, plus the explicit T ⊗ 1 term.
The planar tree-level Δ^c coproduct: explicit T ⊗ 1 term plus
the sum of cut-summand tensors with trace-preserving remainders.
Equations
- One or more equations did not get rendered due to their size.
Instances For
comulCForestPlanar — forest-level Δ^c, multiplicative extension #
The planar forest-level Δ^c: multiplicative product of tree-level coproducts over the components of the forest.
Equations
- RootedTree.ConnesKreimer.comulCForestPlanar τ F = (Multiset.map (RootedTree.ConnesKreimer.comulCTreePlanar τ) F).prod
Instances For
comulCMonoidHomP and comulCAlgHomP — AlgHom packaging #
comulCForestPlanar τ as a monoid hom from
Multiplicative (Forest (Planar (α ⊕ β))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Δ^c coproduct on ConnesKreimer R (Planar (α ⊕ β)) as an
algebra hom, parameterized by the trace encoder τ.
Equations
- One or more equations did not get rendered due to their size.