Δ^c on ConnesKreimer R (Nonplanar (α ⊕ β)) via descent + duality

[MCB25] [foissy-typed-decorated-rooted-trees-2018]

The decorated coproduct Δ^c (contraction-extraction with trace placeholders) descended from the tree-level version comulCAlgHomP in Coproduct/Trace.lean to Nonplanar trees. Coassociativity is proved via Foissy 2018 §4.2 GL-CK duality: GL associativity (product in GrossmanLarson.lean) ⇔ Δ^c coassociativity, transported through the symmetry-weighted pairing in GrossmanLarsonPairing.lean.

MCB target: Lemma 1.2.10

comulCN_coassoc + Bialgebra instance closes MCB Lemma 1.2.10 (the graded bialgebra structure of (V(F_{SO_0}), ⊔, Δ^c)). The GL/duality route is the unification approach that also enables Δ^d (Def 1.2.5, via different extraction policy + projection) and Δ^ρ (Lemma 1.2.11, currently parallel — to be unified at R.8). See memory/project_mcb_unification_rationale.md for why this matters architecturally (avoids ~thousands of LOC of duplication).

The descent layer mirrors Coproduct/PruningNonplanar.lean's descent of Δ^ρ. The duality-based coassoc proof is the new technique that handles Δ^c — for which Foissy clean coassoc (used for Δ^ρ) does NOT work (B+ is not a Hochschild 1-cocycle for Δ^c; see CHANGELOG entry 0.230.944 R.0 patch and project_phase_e3_db_plan.md).

Construction

1. Descent of cutSummandsCP through Nonplanar.mk. Mirrors the Pruning descent but threads the trace-encoder τ.
2. comulCTreeN, comulCForestN, comulCAlgHomN — Nonplanar tree/forest-level Δ^c, packaged as algebra hom.
3. Coassoc via duality (Foissy 2018 §4.2): the duality theorem pairing (gl x y) z = pairing x (Δ^c z) (after suitable ⊗-evaluation) lets us transport gl_assoc (R.5.5) to Δ^c coassoc.
4. Bialgebra instance: counit + counit-multiplicativity from CK, coassoc from duality.

Status

[UPSTREAM] candidate. Sorry-free. MCB Lemma 1.2.10 is fully proved: both its grading content (mcb_lemma_1_2_10) and Δ^c coassociativity (comulCN_coassoc), the latter under the TraceCoherent hypothesis. The coassoc proof is the direct double-cut bijection doubleCut_eq, descended from the tree-level DoubleCut.coassT (Coproduct/TraceCoassoc.lean) through Nonplanar.mk. The earlier plan to derive it from a GL/Δ^c pairing duality was abandoned: that duality is false (GL grafting never removes trace markers, so no orientation of ⟨x ⋆ y, z⟩ = pairing₂ (… ) (Δ^c z) can hold; counterexamples in scratch/validate_duality.lean V4). The duality route works for the deletion variant Δ^ρ — see Coproduct/PruningDuality.lean.

Descent of cut-summand enumeration

Mirrors Coproduct/PruningNonplanar.lean's descent of cutSummandsP, but for the generic cutSummandsG (which uses a List-shaped per-cut remainder rather than Option). The descent applies whenever the extract policy is invariant under RoseTree.PermEquiv modulo Nonplanar.mk. For Δ^c (extractC (τ ∘ Nonplanar.mk)) this follows from value_permEquiv.

Pointwise projection for the G-form

Bridge: projSummand factors through projForestG + node

Combiner factoring

The cons case of cutListSummandsG adds the cut forest and concatenates the remainder lists. At the Nonplanar level (via projForestG), the remainder concatenation becomes multiset addition.

Cartesian-product distributivity (G-form copy)

Headline factoring: cons case of projected cutListSummandsG

Extract-policy invariance

The hypothesis on the extract policy: its return value, projected component-wise through Nonplanar.mk, is the same on PermEquiv-equal inputs. For Δ^c (extractC (τ ∘ Nonplanar.mk)) this holds because the root label and the τ value are both PermEquiv-invariant.

def RootedTree.ConnesKreimer.ExtractInvariant {α : Type u_2} (extract : RoseTree α → Option (List (RoseTree α))) : Prop

An extract policy is Nonplanar.mk-invariant if its return value, projected componentwise through Nonplanar.mk, depends on its input only through Nonplanar.mk.

Equations

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

List-side projection invariants

Three theorems parallel to cutListSummandsP_proj_at_via_augAction, cutListSummandsP_proj_tail_lift, and cutListSummandsP_proj_perm.

Swap symmetry for combinerProjG

Headline: PermStep + EqvGen lift

Structural induction on PermStep. The swapAtRoot case uses cutListSummandsG_proj_perm; the recurse case uses the inductive hypothesis combined with cutListSummandsG_proj_at_via_augAction.

theorem RootedTree.ConnesKreimer.cutSummandsG_proj_permStep {α : Type u_2} {extract : RoseTree α → Option (List (RoseTree α))} (hExt : ExtractInvariant extract) {t s : RoseTree α} (h : t.PermStep s) : Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsG extract t) = Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsG extract s)

Projection invariance under a single PermStep.

theorem RootedTree.ConnesKreimer.cutSummandsG_proj_permEquiv {α : Type u_2} {extract : RoseTree α → Option (List (RoseTree α))} (hExt : ExtractInvariant extract) {t s : RoseTree α} (h : t.PermEquiv s) : Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsG extract t) = Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsG extract s)

Projection invariance under PermEquiv. Pure EqvGen lift.

Trace specialization

The Δ^c policy extractC (τ ∘ Nonplanar.mk) is ExtractInvariant:

• For Sum.inl _-rooted inputs, extractC returns some [traceLeaf (τ (mk t))].
• For Sum.inr _-rooted inputs, extractC returns none.

Both cases are determined by the root label and the τ value, both of which are PermEquiv-invariant.

theorem RootedTree.ConnesKreimer.extractC_mkComp_invariant {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : ExtractInvariant (extractC (τ ∘ Nonplanar.mk))

The Δ^c extract policy is ExtractInvariant.

theorem RootedTree.ConnesKreimer.cutSummandsCP_proj_permEquiv {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) {t s : RoseTree (α ⊕ β)} (h : t.PermEquiv s) : Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsCP (τ ∘ Nonplanar.mk) t) = Multiset.map RootedTree.ConnesKreimer.projSummand✝ (cutSummandsCP (τ ∘ Nonplanar.mk) s)

Δ^c cut-summand-projection invariance under PermEquiv.

Descent of cutSummandsCP through Nonplanar.mk

noncomputable def RootedTree.cutSummandsCN {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : Nonplanar (α ⊕ β) → Multiset (Forest (Nonplanar (α ⊕ β)) × Nonplanar (α ⊕ β))

The Nonplanar Δ^c cut summands, descended from cutSummandsCP via Nonplanar.lift using the descent invariance cutSummandsCP_proj_permEquiv.

Equations

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

@[simp]

theorem RootedTree.cutSummandsCN_mk {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (T : RoseTree (α ⊕ β)) : cutSummandsCN τ (Nonplanar.mk T) = Multiset.map RootedTree.ConnesKreimer.projSummand✝ (ConnesKreimer.cutSummandsCP (τ ∘ Nonplanar.mk) T)

Nonplanar tree- and forest-level Δ^c

noncomputable def RootedTree.comulCTreeN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) : TensorProduct R (ConnesKreimer R (Nonplanar (α ⊕ β))) (ConnesKreimer R (Nonplanar (α ⊕ β)))

The Nonplanar tree-level Δ^c coproduct.

Equations

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

noncomputable def RootedTree.comulCForestN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (F : Forest (Nonplanar (α ⊕ β))) : TensorProduct R (ConnesKreimer R (Nonplanar (α ⊕ β))) (ConnesKreimer R (Nonplanar (α ⊕ β)))

The Nonplanar forest-level Δ^c (multiplicative extension).

Equations

• RootedTree.comulCForestN τ F = (Multiset.map (RootedTree.comulCTreeN τ) F).prod

@[simp]

theorem RootedTree.comulCForestN_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : comulCForestN τ 0 = 1

@[simp]

theorem RootedTree.comulCForestN_add {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (F G : Forest (Nonplanar (α ⊕ β))) : comulCForestN τ (F + G) = comulCForestN τ F * comulCForestN τ G

noncomputable def RootedTree.comulCMonoidHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : Multiplicative (Forest (Nonplanar (α ⊕ β))) →* TensorProduct R (ConnesKreimer R (Nonplanar (α ⊕ β))) (ConnesKreimer R (Nonplanar (α ⊕ β)))

Forest-level Δ^c as a MonoidHom from Multiplicative (Forest ...).

Equations

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

noncomputable def RootedTree.comulCAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] TensorProduct R (ConnesKreimer R (Nonplanar (α ⊕ β))) (ConnesKreimer R (Nonplanar (α ⊕ β)))

The Δ^c coproduct on ConnesKreimer R (Nonplanar (α ⊕ β)) as an algebra hom, parameterized by the trace encoder τ.

Equations

• RootedTree.comulCAlgHomN τ = RootedTree.ConnesKreimer.lift (RootedTree.comulCMonoidHomN τ)

@[simp]

theorem RootedTree.comulCAlgHomN_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (F : Forest (Nonplanar (α ⊕ β))) : (comulCAlgHomN τ) (ConnesKreimer.of' F) = comulCForestN τ F

@[simp]

theorem RootedTree.comulCAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) : (comulCAlgHomN τ) (ConnesKreimer.ofTree T) = comulCTreeN τ T

Tensor-extended pairings

The pairing ⟨·, ·⟩ from GrossmanLarsonPairing.lean extends to the tensor square (pairing₂) and cube (pairing₃). These power the GL/CK duality for the deletion coproduct Δ^ρ (Coproduct/PruningDuality.lean: ⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z)). For the trace variant Δ^c no such duality holds — the trunk of a proper cut contains trace-marker leaves that GL grafting can never produce — so Δ^c coassociativity (comulCN_coassoc below) is a separate combinatorial statement.

noncomputable def RootedTree.pairing₂ {R : Type u_1} [CommSemiring R] {α : Type u_2} : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)) →ₗ[R] TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)) →ₗ[R] R

The tensor-extended pairing H ⊗ H →ₗ H ⊗ H →ₗ R, defined by pairing₂ (x ⊗ y) (w ⊗ z) = pairing x w * pairing y z and extended bilinearly.

Implementation: reshuffle (x⊗y)⊗(w⊗z) to (x⊗w)⊗(y⊗z) via tensorTensorTensorComm; apply TP.map pair pair where pair = TP.lift pairing : H ⊗ H →ₗ R; contract via mul' R R; curry the result.

Decoration-free: works on ConnesKreimer R (Nonplanar α) for any α. Consumed by the Δ^ρ duality (Coproduct/PruningDuality.lean).

Equations

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

@[simp]

theorem RootedTree.pairing₂_tmul_tmul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y w z : ConnesKreimer R (Nonplanar α)) : (pairing₂ (x ⊗ₜ[R] y)) (w ⊗ₜ[R] z) = (GrossmanLarson.pairing x) w * (GrossmanLarson.pairing y) z

Evaluation of pairing₂ on pure tensors: pairing₂ (x ⊗ y) (w ⊗ z) = pairing x w * pairing y z.

noncomputable def RootedTree.pairing₃ {R : Type u_1} [CommSemiring R] {α : Type u_2} : TensorProduct R (ConnesKreimer R (Nonplanar α)) (TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))) →ₗ[R] TensorProduct R (ConnesKreimer R (Nonplanar α)) (TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))) →ₗ[R] R

The triple-tensor pairing H ⊗ (H ⊗ H) →ₗ H ⊗ (H ⊗ H) →ₗ R, defined on pure tensors by pairing₃ (a ⊗ (b ⊗ c)) (x ⊗ (y ⊗ z)) = pairing a x · pairing b y · pairing c z.

Used in the duality-based proof of comulCN_coassoc: equating LHS and RHS coassoc expressions via pairing against arbitrary x ⊗ (y ⊗ z) triple tensors.

Implementation: pairing on the first factor times pairing₂ on the second factor; both extended bilinearly.

Equations

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

@[simp]

theorem RootedTree.pairing₃_tmul_tmul_tmul {R : Type u_1} [CommSemiring R] {α : Type u_2} (a b c x y z : ConnesKreimer R (Nonplanar α)) : (pairing₃ (a ⊗ₜ[R] (b ⊗ₜ[R] c))) (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = (GrossmanLarson.pairing a) x * ((GrossmanLarson.pairing b) y * (GrossmanLarson.pairing c) z)

Evaluation of pairing₃ on pure tensors.

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. Checked computationally in scratch/validate_duality.lean (V4). An earlier sorry-fenced duality statement here was false and has been removed; 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; scratch/validate_duality.lean V5). [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.

def RootedTree.TraceCoherent {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : Prop

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

• RootedTree.TraceCoherent τ = ∀ (T : RootedTree.Nonplanar (α ⊕ β)), ∀ p ∈ RootedTree.cutSummandsCN τ T, τ p.2 = τ T

theorem RootedTree.traceCoherent_const {α : Type u_2} {β : Type u_3} (b : β) : TraceCoherent fun (x : Nonplanar (α ⊕ β)) => b

Constant trace encoders are coherent.

Auxiliary: pairing₃ reduction helpers

Generic reduction lemmas for pairing₃ on shifted tensor shapes, consumed by the Δ^ρ duality chain in Coproduct/PruningDuality.lean.

Helpers: pairing₃ on shifted-tensor forms

Two reduction lemmas that express pairing₃ (x ⊗ (y ⊗ z')) evaluated on shifted tensor forms in terms of pairing₂ and binary pairing. Both are proved by TensorProduct.induction_on, reducing to the pure-tensor case where pairing₃_tmul_tmul_tmul and pairing₂_tmul_tmul agree.

theorem RootedTree.pairing₃_assoc_tmul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y z' : ConnesKreimer R (Nonplanar α)) (U : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))) (c : ConnesKreimer R (Nonplanar α)) : (pairing₃ (x ⊗ₜ[R] (y ⊗ₜ[R] z'))) ((TensorProduct.assoc R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))) (U ⊗ₜ[R] c)) = (pairing₂ (x ⊗ₜ[R] y)) U * (GrossmanLarson.pairing z') c

pairing₃ (x ⊗ (y ⊗ z')) ∘ assoc on a (U ⊗ c)-shape tensor: factors as pairing₂ (x ⊗ y) U * pairing z' c. Generic in α (the trace decoration is irrelevant).

theorem RootedTree.pairing₃_tmul_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y z' a : ConnesKreimer R (Nonplanar α)) (S : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))) : (pairing₃ (x ⊗ₜ[R] (y ⊗ₜ[R] z'))) (a ⊗ₜ[R] S) = (GrossmanLarson.pairing x) a * (pairing₂ (y ⊗ₜ[R] z')) S

pairing₃ (x ⊗ (y ⊗ z')) on a (a ⊗ S)-shape tensor: factors as pairing x a * pairing₂ (y ⊗ z') S. Generic in α.

Chain lemmas: pairing₃ against coassocLHSLin/RHSLin

These compose two applications of pairing_gl_eq_pairing_coproduct_C (Foissy 2018 §4.2) through the helper lemmas above. The intermediate pairing₃_assoc_rTensor_comul / pairing₃_lTensor_comul lemmas generalize over the inner Δ^c-image, enabling a clean specialization to V = Δ^c z.

Nondegeneracy of pairing₂ and pairing₃ (lifted from binary)

pairing₂ and pairing₃ are nondegenerate over [CharZero R] [NoZeroDivisors R], lifted from binary pairing_nondegenerate via the natural basis of CK = (Forest T) →₀ R.

theorem RootedTree.pairing₃_nondegenerate {R : Type u_1} [CommSemiring R] {α : Type u_2} [CharZero R] [NoZeroDivisors R] (U : TensorProduct R (ConnesKreimer R (Nonplanar α)) (TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)))) (h : ∀ (t : TensorProduct R (ConnesKreimer R (Nonplanar α)) (TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)))), (pairing₃ t) U = 0) : U = 0

Nondegeneracy of pairing₃: if U ∈ CK ⊗ (CK ⊗ CK) pairs to zero against every test triple tensor, then U = 0.

Proof: decompose U via the basis on the outer factor as U = c.sum (fun F U_F => of' F ⊗ U_F) where U_F ∈ CK ⊗ CK. Pairing against of' F ⊗ (x ⊗ y) extracts autF · pairing₂ (x ⊗ y) (c F) via pairing₃_of'_tmul_of'_tmul. Over CharZero (so autF ≠ 0), each pairing₂ (x ⊗ y) (c F) = 0 for all x, y; by pairing₂_nondegenerate, c F = 0. Hence c = 0 and U = 0.

Equality form of nondegeneracy

pairing₃_unique: two tensors that pair the same against every test vector are equal. Follows from pairing₃_nondegenerate via U = V ↔ U - V = 0, requiring AddCommGroup on the triple tensor.

Single ring hypothesis: this theorem lives in its own section with [CommRing R₁] only (NOT [CommSemiring R] from the file's top section + [CommRing R] added on top — those create two CommSemiring R instances that don't unify). The AddCommGroup on the wrapper comes from the global ConnesKreimer.instCommRing.

theorem RootedTree.pairing₃_unique {R₁ : Type u_4} [CommRing R₁] {α₁ : Type u_5} [CharZero R₁] [NoZeroDivisors R₁] (U V : TensorProduct R₁ (ConnesKreimer R₁ (Nonplanar α₁)) (TensorProduct R₁ (ConnesKreimer R₁ (Nonplanar α₁)) (ConnesKreimer R₁ (Nonplanar α₁)))) (h : ∀ (t : TensorProduct R₁ (ConnesKreimer R₁ (Nonplanar α₁)) (TensorProduct R₁ (ConnesKreimer R₁ (Nonplanar α₁)) (ConnesKreimer R₁ (Nonplanar α₁)))), (pairing₃ t) U = (pairing₃ t) V) : U = V

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 plan (validated computationally, scratch/validate_duality.lean V7):

1. comulCTreeN/comulCForestN as multiset sums over cut enumerators treeCutsN/forestCutsN (this section).
2. Each composite expands to a sum over a double-cut enumerator dcLHS/dcRHS (lhsExpand/rhsExpand).
3. dcLHS = dcRHS as Nonplanar multisets under coherence (doubleCut_eq, the bijection).

instance RootedTree.instLeftCommConvCut {α : Type u_5} {β : Type u_6} : LeftCommutative fun (s acc : Multiset (Forest (Nonplanar (α ⊕ β)) × Forest (Nonplanar (α ⊕ β)))) => Multiset.map RootedTree.ConnesKreimer.combinerProjG✝ (s ×ˢ acc)

Convolution-of-cuts is left-commutative (it is the symmetric combinerProjG of the descent layer); needed for Multiset.foldr.

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.

theorem RootedTree.comulCN_coassoc_tree {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') (hτ : TraceCoherent τ) (T : Nonplanar (α' ⊕ β')) : (TensorProduct.assoc R' (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β')))) ((LinearMap.rTensor (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap) (comulCTreeN τ T)) = (LinearMap.lTensor (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap) (comulCTreeN τ T)

Per-tree Δ^c coassociativity (LinearMap-applied form on a single tree's coproduct comulCTreeN τ T). The combinatorial heart of coassociativity: both sides enumerate ordered pairs of nested admissible cuts of T, and TraceCoherent τ makes the trunk-marker labels written by the two cut orders agree.

Reduced by the two expansion lemmas (lhsExpand, rhsExpand) to the double-cut bijection doubleCut_eq. The headline comulCN_coassoc reduces to this by multiplicativity (forest = product of trees).

theorem RootedTree.comulCN_coassoc {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') (hτ : TraceCoherent τ) : ↑(TensorProduct.assoc R' (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β')))) ∘ₗ LinearMap.rTensor (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap ∘ₗ (comulCAlgHomN τ).toLinearMap = LinearMap.lTensor (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap ∘ₗ (comulCAlgHomN τ).toLinearMap

Coassociativity of comulCAlgHomN (Δ^c on Nonplanar), 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; validated in scratch/validate_duality.lean V5). 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 GrossmanLarson.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).

Empty-cut uniqueness — combinatorial substrate for the per-tree counit law

For any extract policy and tree T, the unique cut summand of cutSummandsG extract T with empty cut forest (p.1.card = 0) is the empty cut (0, T). By mutual structural induction with the list and per-child cases. This is the substrate for the Δ^c per-tree counit law: under (counit ⊗ id), only this summand survives, contributing 1 ⊗ ofTree T.

Counit laws + Bialgebra instance

With comulCN_coassoc structurally closed (modulo 4 deferred substrate sorries), the remaining inputs to Bialgebra.ofAlgHom are:

1. The AlgHom-form coassoc (comulCAlgHomN_coassoc_algHom).
2. The right counit law (counit_rTensor_comulCAlgHomN).
3. The left counit law (counit_lTensor_comulCAlgHomN).

Each lands here. The per-tree counit laws are derived from the empty-cut uniqueness substrate (cutSummandsCN_filter_empty) above.

theorem RootedTree.comulCAlgHomN_coassoc_algHom {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') (hτ : TraceCoherent τ) : (↑(Algebra.TensorProduct.assoc R' R' R' (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β'))) (ConnesKreimer R' (Nonplanar (α' ⊕ β'))))).comp ((Algebra.TensorProduct.map (comulCAlgHomN τ) (AlgHom.id R' (ConnesKreimer R' (Nonplanar (α' ⊕ β'))))).comp (comulCAlgHomN τ)) = (Algebra.TensorProduct.map (AlgHom.id R' (ConnesKreimer R' (Nonplanar (α' ⊕ β')))) (comulCAlgHomN τ)).comp (comulCAlgHomN τ)

AlgHom-form coassoc of comulCAlgHomN under trace coherence. Follows from comulCN_coassoc by AlgHom extensionality.

Counit laws — factored via per-tree + forest helpers

Mirrors the Δ^ρ proof structure in PruningNonplanar.lean (lines 1049-1598). The headline theorems are CLOSED structurally from two per-tree sorries that capture the cutSummandsCN substrate work (the (0, T) summand + non-zero-p₁ killing under counit ⊗ id).

theorem RootedTree.counit_rTensor_comulCAlgHomN {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') : (Algebra.TensorProduct.map ConnesKreimer.counit (AlgHom.id R' (ConnesKreimer R' (Nonplanar (α' ⊕ β'))))).comp (comulCAlgHomN τ) = ↑(Algebra.TensorProduct.lid R' (ConnesKreimer R' (Nonplanar (α' ⊕ β')))).symm

Right counit law (CLOSED via per-tree + forest helpers): (counit ⊗ id) ∘ Δ^c = lid⁻¹.

theorem RootedTree.counit_lTensor_comulCAlgHomN {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') : (Algebra.TensorProduct.map (AlgHom.id R' (ConnesKreimer R' (Nonplanar (α' ⊕ β')))) ConnesKreimer.counit).comp (comulCAlgHomN τ) = ↑(Algebra.TensorProduct.rid R' R' (ConnesKreimer R' (Nonplanar (α' ⊕ β')))).symm

Left counit law (CLOSED via per-tree + forest helpers): (id ⊗ counit) ∘ Δ^c = rid⁻¹.

@[reducible]

noncomputable def RootedTree.bialgebraC {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : Nonplanar (α' ⊕ β') → β') (hτ : TraceCoherent τ) : Bialgebra R' (ConnesKreimer R' (Nonplanar (α' ⊕ β')))

Bialgebra structure on ConnesKreimer R' (Nonplanar (α' ⊕ β')) with Δ^c as the coproduct, for a trace-coherent encoder.

The graded bialgebra structure of MCB Lemma 1.2.10. Built via Bialgebra.ofAlgHom with comulCAlgHomN τ as the coproduct and the inherited counit from CK. A def, not an instance: coassociativity needs TraceCoherent τ (it is false for arbitrary τ — see comulCN_coassoc), which instance resolution cannot synthesize. Depends on:

• comulCAlgHomN_coassoc_algHom (sorried, under trace coherence).
• counit_rTensor_comulCAlgHomN (proved).
• counit_lTensor_comulCAlgHomN (proved).

Equations

• RootedTree.bialgebraC τ hτ = Bialgebra.ofAlgHom (RootedTree.comulCAlgHomN τ) RootedTree.ConnesKreimer.counit ⋯ ⋯ ⋯

MCB Lemma 1.2.10 — graded bialgebra structure

Per marcolli-chomsky-berwick-2025 p. 37, Lemma 1.2.10:

Let V^c(𝔉_{SO_0}) denote the vector space (over ℚ) spanned by the workspaces F ∈ 𝔉_{SO_0}, endowed with the product given by the disjoint union ⊔ and the coproduct Δ^c of (1.2.8). The space V(𝔉_{SO_0}) is graded by the number of edges. Then (V^c(𝔉_{SO_0}), ⊔, Δ^c) is a graded bialgebra.

This section formalizes the statement: defines edge-count grading on forests, sets up the graded subspaces, and packages MCB Lemma 1.2.10 as a theorem combining the Δ^c bialgebra structure (bialgebraC, for trace-coherent encoders) with grading compatibility. Both grading halves are fully proved (edge conservation through the trace cut machinery: cutSummandsCN_numNodes).

def RootedTree.Forest.edgeCount {X : Type u_7} (F : Forest (Nonplanar X)) : ℕ

Edge count of a forest: total edges across all trees.

A tree with n vertices has n - 1 edges. For a forest F = {T_1, ..., T_k}: total edges = Σ (weight(T_i) - 1).

Defined as a per-tree sum (avoiding global subtraction) to make additivity (edgeCount (F + G) = edgeCount F + edgeCount G) immediate from Multiset.map_add + Multiset.sum_add.

Per MCB Lemma 1.2.10, this is the grading on V^c(𝔉_{SO_0}).

Equations

• F.edgeCount = (Multiset.map (fun (T : RootedTree.Nonplanar X) => T.numNodes - 1) F).sum

noncomputable def RootedTree.gradedPiece {R'' : Type u_4} [CommRing R''] (X : Type u_7) (n : ℕ) : Submodule R'' (ConnesKreimer R'' (Nonplanar X))

Graded piece V_n: the subspace of ConnesKreimer R'' (Nonplanar X) spanned by forests with exactly n edges.

Equations

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

Edge bookkeeping for edgeCount

Homogeneous tensor span at fixed total edge degree

theorem RootedTree.mcb_lemma_1_2_10 {R'' : Type u_4} [CommRing R''] {α'' : Type u_5} {β'' : Type u_6} (τ : Nonplanar (α'' ⊕ β'') → β'') : (∀ (F G : Forest (Nonplanar (α'' ⊕ β''))), (F + G).edgeCount = F.edgeCount + G.edgeCount) ∧ ∀ (n : ℕ) (F : Forest (Nonplanar (α'' ⊕ β''))), F.edgeCount = n → (comulCAlgHomN τ) (ConnesKreimer.of' F) ∈ Submodule.span R'' {y : TensorProduct R'' (ConnesKreimer R'' (Nonplanar (α'' ⊕ β''))) (ConnesKreimer R'' (Nonplanar (α'' ⊕ β''))) | ∃ (i : ℕ) (j : ℕ) (_ : i + j = n) (xi : ConnesKreimer R'' (Nonplanar (α'' ⊕ β''))) (yi : ConnesKreimer R'' (Nonplanar (α'' ⊕ β''))), xi ∈ gradedPiece (α'' ⊕ β'') i ∧ yi ∈ gradedPiece (α'' ⊕ β'') j ∧ y = xi ⊗ₜ[R''] yi}

MCB Lemma 1.2.10 — the graded bialgebra structure.

States that:

1. The bialgebra structure bialgebraC (from comulCAlgHomN, for trace-coherent encoders).
2. The space V^c(𝔉_{SO_0}) is graded by edgeCount.
3. The product (⊔ = disjoint union) preserves grading additively: V_n ⊗ V_m → V_{n+m} (because edgeCount(F + G) = edgeCount(F) + edgeCount(G)).
4. The coproduct (Δ^c) preserves grading: for x ∈ V_n, Δ^c(x) ∈ Σ_{i+j=n} V_i ⊗ V_j.

Status: statement packaged. The grading-compatibility proofs are sorry'd (substrate work).

Hopf structure (corollary, deferred):

induces a Hopf algebra structure on the complement in V^c(𝔉_{SO_0}) of the span of the lexical items and features.

Antipode emerges via the graded connected bialgebra construction (inductive formula S(x) = -x - Σ S(x_(1)) · x_(2)) after quotienting by the (1 - α) ideal for α a lexical-item generator. Deferred to sibling file.