Δ^c on ConnesKreimer R (Nonplanar (α ⊕ β)) via descent #
[MCB25] [foissy-typed-decorated-rooted-trees-2018]
The decorated coproduct Δ^c (contraction-extraction with trace
placeholders), built on the descended cut enumeration cutSummandsCN
(Core/Combinatorics/RootedTree/Cut.lean), with its coassociativity,
counit laws, and Bialgebra packaging. Together with the edge grading
in Coproduct/TraceGrading.lean this closes
[MCB25] Lemma 1.2.10, the graded bialgebra
structure of (V(F_{SO_0}), ⊔, Δ^c).
Construction #
comulCTreeN,comulCForestN,comulCAlgHomN— Nonplanar tree/forest-level Δ^c, packaged as algebra hom. The descent layer mirrorsCoproduct/Pruning.lean's descent of Δ^ρ.- Coassociativity (
comulCN_coassoc, underTraceCoherent) by the direct double-cut bijection: both composites expand to sums over double-cut enumerators (lhsExpand/rhsExpand), which agree under trace coherence (doubleCut_eq), descended from the planarDoubleCut.coassT(Core/Combinatorics/RootedTree/DoubleCut.lean) throughNonplanar.mk. - Counit laws from the empty-cut uniqueness of the enumeration
(
cutSummandsCN_filter_empty,Core/Combinatorics/RootedTree/Cut.lean). instIsAdmissibleCutsCN— the laws packaged asIsAdmissibleCuts (cutSummandsCN τ), gated onFact (TraceCoherent τ), soWithCuts R (cutSummandsCN τ)carries the Δ^cBialgebrainstance (Coproduct/WithCuts.lean).
No GL/Δ^c duality #
The GL/CK pairing duality that proves Δ^ρ coassociativity in
Coproduct/PruningDuality.lean is false for Δ^c: GL grafting never
removes trace markers, so no orientation of
⟨x ⋆ y, z⟩ = pairing₂ (…) (Δ^c z) can hold, and B+ is not a Hochschild
1-cocycle for Δ^c either (see the Trace-coherence section below). The
pairings themselves live in GrossmanLarson/Pairing.lean.
Status #
[UPSTREAM] candidate.
Nonplanar tree- and forest-level Δ^c #
Definitional instantiations of the generic admissible-cut coproduct
(Coproduct/WithCuts.lean) at the Δ^c enumeration cutSummandsCN τ.
The Nonplanar tree-level Δ^c coproduct: comulTreeNG at
cuts := cutSummandsCN τ.
Instances For
The Nonplanar forest-level Δ^c (multiplicative extension).
Equations
Instances For
Forest-level Δ^c as a MonoidHom from Multiplicative (Forest ...).
Equations
Instances For
The Δ^c coproduct on ConnesKreimer R (Nonplanar (α ⊕ β)) as
an algebra hom: comulAlgHomNG at cuts := cutSummandsCN τ,
parameterized by the trace encoder τ.
Equations
Instances For
Trace coherence #
There is no GL/Δ^c pairing duality: for any marker-free z with a
proper admissible cut, the trunk side of Δ^c z carries trace-marker
leaves, while every forest in the support of a GL product x ⋆ y has at
least as many markers as x and y combined (grafting never removes
vertices) — so ⟨x ⋆ y, z⟩ = 0 against any cut summand that would make
the right side nonzero, in either slot orientation. The duality (with
crossed slots) is true for the deletion variant Δ^ρ and is proved in
Coproduct/PruningDuality.lean.
Δ^c coassociativity itself is not τ-generic either: iterating Δ^c
re-encodes already-cut subtrees, so the marker written by a second-stage
cut is τ of a tree containing markers, while the opposite cut order
writes τ of the original subtree. For τ sensitive to that difference
coassociativity fails (counterexample: τ = count of Sum.inl
vertices, z an inl-labeled 3-chain).
[MCB25]'s proof of Lemma 1.2.10 (book
p. 37–38) silently uses that their trace labels compose under
contraction ("the accessible terms of accessible terms … are themselves
accessible terms"); TraceCoherent is that hypothesis made explicit.
Trace coherence: τ does not distinguish a cut trunk (with its
trace markers) from the tree it was cut from. This is the condition
under which iterated Δ^c cuts commute (coassociativity): second-stage
markers computed on marked trunks agree with markers computed on the
original tree. Constant encoders satisfy it (traceCoherent_const);
[MCB25]'s identity trace satisfies it in
spirit via label expansion (their marker labels denote subtrees of
the original tree).
Equations
- ConnesKreimer.TraceCoherent τ = ∀ (T : RoseTree.Nonplanar (α ⊕ β)), ∀ p ∈ ConnesKreimer.cutSummandsCN τ T, τ p.2 = τ T
Instances For
Constant trace encoders are coherent.
Double-cut enumeration — substrate for the direct coassoc proof #
The combinatorial core of Δ^c coassociativity (comulCN_coassoc_tree),
following the [MCB25] Lemma 1.2.10 argument
("the accessible terms of accessible terms … are themselves accessible
terms"). Both (Δ^c ⊗ id) ∘ Δ^c and (id ⊗ Δ^c) ∘ Δ^c enumerate
ordered pairs of nested admissible cuts of a tree; the two enumerations
biject under TraceCoherent.
The proof structure:
comulCTreeN/comulCForestNas multiset sums over cut enumeratorstreeCutsN/forestCutsN(this section).- Each composite expands to a sum over a double-cut enumerator
dcLHS/dcRHS(lhsExpand/rhsExpand). dcLHS = dcRHSas Nonplanar multisets under coherence (doubleCut_eq, the bijection).
Descent of the double-cut enumerators through Nonplanar.mk #
The Nonplanar dcLHS/dcRHS are the projections (via Nonplanar.mk) of the
tree-level DoubleCut.dcLHSP/dcRHSP; DoubleCut.coassT then gives the bijection.
Coassociativity of Δ^c on Nonplanar (direct double-cut bijection) #
Specialized to [CommRing R] (rather than [CommSemiring R]) only for
uniformity with the Bialgebra consumers; the double-cut proof itself is
CommSemiring-generic.
Per-tree Δ^c coassociativity: both composites enumerate ordered pairs
of nested admissible cuts of T, and TraceCoherent τ makes the
trunk-marker labels written by the two cut orders agree.
Coassociativity of Δ^c under trace coherence.
NOT τ-generic: without TraceCoherent τ, iterating Δ^c writes
second-stage markers computed on marked trunks, and the two cut
orders disagree (counterexample: τ = inl-vertex count on an
inl-labeled 3-chain). Under coherence the double-cut enumerations
agree — this is
[MCB25] Lemma 1.2.10's coassociativity
(book p. 37–38, the quotient-composition argument "the accessible
terms of accessible terms … are themselves accessible terms").
Proved by the double-cut bijection on each tree
(comulCN_coassoc_tree), lifted to forests by multiplicativity
(both composites are algebra homs, so they agree on a product
of' F = ∏ ofTree Tᵢ once they agree on each ofTree Tᵢ). The
earlier plan to transport mul_assoc through a
GL/Δ^c pairing duality is dead — that duality is false (see the
Trace coherence section above); the duality route works only for
Δ^ρ (Coproduct/PruningDuality.lean).
Counit laws + Bialgebra instance #
The three inputs to Bialgebra.ofAlgHom:
- The AlgHom-form coassoc (
comulCAlgHomN_coassoc_algHom). - The right counit law (
counit_rTensor_comulCAlgHomN). - The left counit law (
counit_lTensor_comulCAlgHomN).
The per-tree counit laws are derived from the empty-cut uniqueness of
the enumeration (cutSummandsCN_filter_empty,
Core/Combinatorics/RootedTree/Cut.lean).
The AlgHom form of Δ^c coassociativity under trace coherence.
Counit laws — factored via per-tree + forest helpers #
Mirrors the Δ^ρ proof structure in Coproduct/Pruning.lean:
per-tree laws from empty-cut uniqueness, lifted to forests by
multiplicativity. Stated over CommSemiring (unlike the coassoc, which
needs a ring) so they can feed the ring-uniform IsAdmissibleCuts
counit fields directly.
The right counit law for Δ^c.
The left counit law for Δ^c.
Δ^c is the generic coproduct at cuts := cutSummandsCN τ — definitional.
Δ^c is an admissible cut policy for a trace-coherent encoder:
comulCAlgHomN_coassoc_algHom and the counit laws packaged as the
IsAdmissibleCuts mixin, so WithCuts R (cutSummandsCN τ) receives its
Bialgebra instance — the bialgebra structure of MCB Lemma 1.2.10.
Gated on Fact (TraceCoherent τ): coassociativity is false for
arbitrary τ (see comulCN_coassoc), and instance resolution cannot
synthesize the coherence hypothesis without the Fact wrapper.