Δ^ρ on ConnesKreimer R (Nonplanar α) via projection from RoseTree

[MCB25] [foissy-introduction-hopf-algebras-trees]

The Nonplanar Δ^ρ is obtained by descending the tree-level Δ^ρ (Coproduct.lean) through the projection mk : RoseTree α → Nonplanar α. The descent requires showing that the projected cut summands ((cutSummandsP T).map projSummand) depend on T : RoseTree α only through mk T, i.e., are invariant under RoseTree.PermEquiv. Once established, Nonplanar.lift produces cutSummandsN, which extends to comulTreeN, comulForestN, and the algebra hom comulAlgHomN.

Status

[UPSTREAM] candidate. Sorry-free. Covers: the descent (comulAlgHomN), the Hochschild 1-cocycle (comulTreeN_node_cocycle, comulAlgHomN_bPlusLin_cocycle), and the counit laws (counit_rTensor_comulAlgHomN, counit_lTensor_comulAlgHomN).

The GL/CK duality theorem (pairing_gl_eq_pairing_coproduct_Rho, classical result of [Foi02]), coassociativity (comulRhoN_coassoc → comulAlgHomN_coassoc_algHom), and the Bialgebra (ConnesKreimer R (Nonplanar α)) instance live downstream in Coproduct/PruningDuality.lean (the duality proof needs the B⁻ calculus of BMinus.lean, which imports this file). The full HopfAlgebra instance (with antipode) lives in the sibling HopfAlgebraNonplanar.lean (Phase A.8).

Architecture

• Projection algebra hom (planarToNonplanarAlg): directly on top of mathlib's AddMonoidAlgebra.mapDomainAlgHom, applied to the additive monoid hom Multiset.mapAddMonoidHom Nonplanar.mk. The universal property of AddMonoidAlgebra does the heavy lifting.
• Cut-summand descent (§3): pointwise projection (projSummand/projForest/projAugAction) plus a clean factoring of the cutListSummandsP cons case as a Nonplanar-level cartesian product (cutListSummandsP_cons_proj); structural induction on PermStep for the headline invariance, with pure EqvGen/Forall₂ lifts for PermEquiv and List.Forall₂ versions.

Projection algebra hom RoseTree → Nonplanar

Nonplanar.mk : RoseTree α → Nonplanar α extends to an algebra hom on ConnesKreimer R via AddMonoidAlgebra.mapDomainAlgHom. Surjective at the carrier level; the kernel encodes PermEquiv-equivalence of forests of trees, which is what subsequent sub-phases will need to factor through.

noncomputable def RootedTree.ConnesKreimer.forestProjAddHom {α : Type u_2} : Forest (RoseTree α) →+ Forest (Nonplanar α)

The additive monoid hom from forests of tree-level trees to forests of nonplanar trees, given by mapping Nonplanar.mk componentwise.

Equations

• RootedTree.ConnesKreimer.forestProjAddHom = Multiset.mapAddMonoidHom RootedTree.Nonplanar.mk

noncomputable def RootedTree.ConnesKreimer.planarToNonplanarAlg {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (RoseTree α) →ₐ[R] ConnesKreimer R (Nonplanar α)

The projection algebra hom ConnesKreimer R (RoseTree α) →ₐ[R] ConnesKreimer R (Nonplanar α) induced by Nonplanar.mk.

Equations

• RootedTree.ConnesKreimer.planarToNonplanarAlg = RootedTree.ConnesKreimer.mapDomainAlgHom RootedTree.ConnesKreimer.forestProjAddHom

API lemmas — action on of' and ofTree

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (RoseTree α)) : planarToNonplanarAlg (of' F) = of' (Multiset.map Nonplanar.mk F)

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (t : RoseTree α) : planarToNonplanarAlg (ofTree t) = ofTree (Nonplanar.mk t)

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_one {R : Type u_1} [CommSemiring R] {α : Type u_2} : planarToNonplanarAlg 1 = 1

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ConnesKreimer R (RoseTree α)) : planarToNonplanarAlg (x * y) = planarToNonplanarAlg x * planarToNonplanarAlg y

Phase A.7-β — projection of cut summands, descent of Δ^ρ

To descend Δ^ρ from RoseTree to Nonplanar, we need a Nonplanar-side cut-summand multiset that is PermEquiv-invariant. The strategy: project each tree-level cut summand through mk componentwise, then prove the resulting multiset depends on T : RoseTree α only through mk T.

The proof factors through three layers:

• Pointwise projection (projSummand, projForest, projAugAction): the per-element Nonplanar.mk lifts.
• Combine factoring (cutListSummandsP_cons_proj): the cons case of cutListSummandsP distributes over the projection, giving a clean cartesian-product recursion at the Nonplanar level.
• Headline lifts (cutSummandsP_proj_permStep, cutSummandsP_proj_permEquiv, cutListSummandsP_proj_componentwise): structural induction on PermStep for the substantive content; pure EqvGen / Forall₂ lifts for the rest.

Pointwise projection

def RootedTree.ConnesKreimer.projSummand {α : Type u_2} : Forest (RoseTree α) × RoseTree α → Forest (Nonplanar α) × Nonplanar α

Project a tree-level cut summand to a nonplanar one.

Equations

• RootedTree.ConnesKreimer.projSummand p = (Multiset.map RootedTree.Nonplanar.mk p.1, RootedTree.Nonplanar.mk p.2)

def RootedTree.ConnesKreimer.projForest {α : Type u_2} : Forest (RoseTree α) × List (RoseTree α) → Forest (Nonplanar α) × Multiset (Nonplanar α)

Project a cutListSummandsP summand to nonplanar level, discarding the list-order of the remainder children. The discarded order doesn't affect the eventual mk (.node a remainder), since mk is invariant under children-list permutation (RoseTree.permEquiv_root_perm).

Equations

• RootedTree.ConnesKreimer.projForest p = (Multiset.map RootedTree.Nonplanar.mk p.1, ↑(List.map RootedTree.Nonplanar.mk p.2))

def RootedTree.ConnesKreimer.projAugAction {α : Type u_2} : Forest (RoseTree α) × Option (RoseTree α) → Forest (Nonplanar α) × Option (Nonplanar α)

Project an augActionP summand to nonplanar level (per-child decision).

Equations

• RootedTree.ConnesKreimer.projAugAction p = (Multiset.map RootedTree.Nonplanar.mk p.1, Option.map RootedTree.Nonplanar.mk p.2)

theorem RootedTree.ConnesKreimer.projSummand_node_factors {α : Type u_2} (a : α) (p : Forest (RoseTree α) × List (RoseTree α)) : projSummand (p.1, RoseTree.node a p.2) = ((projForest p).1, Nonplanar.node a (projForest p).2)

Bridge: applying cutSummandsP_node's wrapper (p.1, .node a p.2) then projSummand factors through projForest followed by the Nonplanar.node a smart constructor.

Combine factoring through projection

The cons case of cutListSummandsP combines a per-child decision (augActionP) with the cut-summands of the remaining children. This combination distributes over the Nonplanar projection: the "projected combiner" innerCombinerProj operates on (Forest × Option) × (Forest × Multiset) and matches projForest of the inline tree-level combiner. The headline result is cutListSummandsP_cons_proj, which expresses the cons case of the projected cutListSummandsP as a clean cartesian product at the Nonplanar level.

Cartesian-product distributivity

The pair-componentwise Prod.map distributes over Multiset.product (×ˢ). Mathlib has the bind-side analogues but not this exact form for multiset products; the proof is one inductive line via cons_product.

Headline factoring: cons case of projected cutListSummandsP

List-side projection invariants

These three theorems establish that the projected cutListSummandsP is invariant under (1) substituting an "augAction-projection-equal" child, (2) substituting a "projForest-equal" tail, and (3) any list permutation.

theorem RootedTree.ConnesKreimer.cutListSummandsP_proj_perm {α : Type u_2} {cs ds : List (RoseTree α)} (h : cs.Perm ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

The projected cutListSummandsP is List.Perm-invariant: two permutation-related child lists yield the same projected cut-summand multiset.

Headline: PermStep + EqvGen lift

Substantive content: cutSummandsP_proj_permStep proves projection invariance under a single elementary step (PermStep). The PermEquiv (EqvGen) and Forall₂ versions follow as straightforward lifts. The structural induction on PermStep handles the recursion: the recurse case calls itself on a strictly smaller child tree.

theorem RootedTree.ConnesKreimer.cutSummandsP_proj_permStep {α : Type u_2} {t s : RoseTree α} (h : t.PermStep s) : Multiset.map projSummand (cutSummandsP t) = Multiset.map projSummand (cutSummandsP s)

Projection invariance under a single PermStep. Structural induction on the step constructor: swapAtRoot uses cutListSummandsP_proj_perm; recurse uses the inductive hypothesis combined with cutListSummandsP_proj_at_via_augAction.

theorem RootedTree.ConnesKreimer.cutSummandsP_proj_permEquiv {α : Type u_2} {t s : RoseTree α} (h : t.PermEquiv s) : Multiset.map projSummand (cutSummandsP t) = Multiset.map projSummand (cutSummandsP s)

Projection invariance under PermEquiv. Pure EqvGen lift of cutSummandsP_proj_permStep.

theorem RootedTree.ConnesKreimer.cutListSummandsP_proj_componentwise {α : Type u_2} {cs ds : List (RoseTree α)} (h : List.Forall₂ RoseTree.PermEquiv cs ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

Componentwise PermEquiv invariance for child lists. Pure Forall₂ induction using cutListSummandsP_proj_at_via_augAction on the head and the IH on the tail.

Δ^ρ on Nonplanar via descent

The cutSummandsP_proj_permEquiv invariance lifts cutSummandsP through Nonplanar.lift, giving a well-defined cutSummandsN. The tree-level coproduct comulTreeN then extends multiplicatively to a forest-level monoid hom and finally to the algebra hom comulAlgHomN.

noncomputable def RootedTree.ConnesKreimer.cutSummandsN {α : Type u_2} : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)

The Nonplanar cut-summand multiset, defined via Nonplanar.lift using the cutSummandsP_proj_permEquiv invariance.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsN_mk {α : Type u_2} (T : RoseTree α) : cutSummandsN (Nonplanar.mk T) = Multiset.map projSummand (cutSummandsP T)

noncomputable def RootedTree.ConnesKreimer.comulTreeN {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

The nonplanar tree-level Δ^ρ: explicit T ⊗ 1 term plus the sum of cut-summand tensors at the Nonplanar level.

Equations

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

noncomputable def RootedTree.ConnesKreimer.comulTreeNFiltered {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) (pred : Forest (Nonplanar α) × Nonplanar α → Prop) [DecidablePred pred] : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

A filtered nonplanar tree-level Δ^ρ: the T ⊗ 1 primitive term plus the cut-summand sum restricted to summands satisfying pred. Generalizes comulTreeN (the pred = always-true case); used to carve phase-restricted sub-coproducts (e.g. the phase coproduct Δ^c_Φ of [MCB25] §1.14).

Equations

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

theorem RootedTree.ConnesKreimer.comulTreeNFiltered_eq_comulTreeN {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) (pred : Forest (Nonplanar α) × Nonplanar α → Prop) [DecidablePred pred] (hAll : ∀ p ∈ cutSummandsN T, pred p) : comulTreeNFiltered T pred = comulTreeN T

The filter drops nothing when every cut summand satisfies pred, recovering the full comulTreeN.

noncomputable def RootedTree.ConnesKreimer.comulForestN {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Nonplanar α)) : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

The nonplanar forest-level Δ^ρ: multiplicative product of tree-level coproducts over the components of the forest.

Equations

• RootedTree.ConnesKreimer.comulForestN F = (Multiset.map RootedTree.ConnesKreimer.comulTreeN F).prod

@[simp]

theorem RootedTree.ConnesKreimer.comulForestN_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulForestN 0 = 1

@[simp]

theorem RootedTree.ConnesKreimer.comulForestN_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Nonplanar α)) : comulForestN (F + G) = comulForestN F * comulForestN G

@[simp]

theorem RootedTree.ConnesKreimer.comulForestN_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) : comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F

Recursive formula: comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F.

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

comulForestN packaged as a MonoidHom from Multiplicative (Forest (Nonplanar α)).

Equations

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

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

The Δ^ρ coproduct on ConnesKreimer R (Nonplanar α) as an algebra hom.

Equations

• RootedTree.ConnesKreimer.comulAlgHomN = RootedTree.ConnesKreimer.lift RootedTree.ConnesKreimer.comulMonoidHomN

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomN_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Nonplanar α)) : comulAlgHomN (of' F) = comulForestN F

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : comulAlgHomN (ofTree T) = comulTreeN T

Phase A.7-γ — Hochschild 1-cocycle for B+_a

B+_a : Forest (Nonplanar α) → Nonplanar α is the smart constructor Nonplanar.node a. Linearly extended to bPlusLin a : H →ₗ[R] H (sending basis element of' F to ofTree (Nonplanar.node a F)), it satisfies the Hochschild 1-cocycle property (Foissy / MCB §1.2.11):

Δ^ρ ∘ B+_a = (·) ⊗ 1 ∘ B+_a + (id ⊗ B+_a) ∘ Δ^ρ

i.e., for every x : H:

Δ^ρ (B+_a x) = (B+_a x) ⊗ 1 + (id ⊗ B+_a)(Δ^ρ x).

This is the algebraic input to Foissy's clean inductive proof of coassociativity (§A.7-δ): the subalgebra A := {x | (Δ ⊗ id)(Δ x) = (id ⊗ Δ)(Δ x)} is closed under B+_a, contains all leaves (which are B+_a 1), hence equals the whole algebra.

B+_a as a function, smart constructor, and linear map

noncomputable def RootedTree.ConnesKreimer.bPlus {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : Nonplanar α

The B+_a operator: graft an unordered forest of Nonplanar trees under a new root labeled a. Identical to the smart constructor.

Equations

• RootedTree.ConnesKreimer.bPlus a F = RootedTree.Nonplanar.node a F

@[simp]

theorem RootedTree.ConnesKreimer.bPlus_def {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : bPlus a F = Nonplanar.node a F

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

The B+_a linear map: linearly extend the smart constructor bPlus a to an R-linear endomorphism of ConnesKreimer R (Nonplanar α), sending the basis element of' F to ofTree (Nonplanar.node a F).

Equations

• RootedTree.ConnesKreimer.bPlusLin a = RootedTree.ConnesKreimer.linearLift fun (F : RootedTree.Forest (RootedTree.Nonplanar α)) => RootedTree.ConnesKreimer.ofTree (RootedTree.Nonplanar.node a F)

@[simp]

theorem RootedTree.ConnesKreimer.bPlusLin_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : (bPlusLin a) (of' F) = ofTree (Nonplanar.node a F)

@[simp]

theorem RootedTree.ConnesKreimer.bPlusLin_one {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : (bPlusLin a) 1 = ofTree (Nonplanar.leaf a)

augActionN and cutForestSummandsN substrate

cutForestSummandsN F is the Nonplanar-level multiset of (cut_forest, remainder_forest) pairs ranging over per-tree decisions on the forest F. Each per-tree decision (augActionN T) is either "extract T whole" (pair ({T}, none)) or "recurse with a cut summand of T" (pair (s.1, some s.2) for s ∈ cutSummandsN T).

Defined recursively at the Nonplanar level via Multiset.foldr, with the LeftCommutative obligation discharged by swap_double_combinerProj (the per-tree-decision swap symmetry, established for the tree-level projection in §3 above and reused here verbatim).

noncomputable def RootedTree.ConnesKreimer.augActionN {α : Type u_2} (T : Nonplanar α) : Multiset (Forest (Nonplanar α) × Option (Nonplanar α))

Per-tree decision multiset at the Nonplanar level: extract this tree whole (({T}, none)), or recurse into a cut summand.

Equations

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

noncomputable def RootedTree.ConnesKreimer.cutForestSummandsN {α : Type u_2} (F : Forest (Nonplanar α)) : Multiset (Forest (Nonplanar α) × Forest (Nonplanar α))

The forest cut summand multiset: every per-tree decision tuple on F : Forest (Nonplanar α) produces a pair (cut_forest, remainder_forest), and cutForestSummandsN F enumerates them all (as a multiset). The public Nonplanar-level analog of (cutListSummandsP ps).map projForest, independent of the tree-level list representation.

Equations

• RootedTree.ConnesKreimer.cutForestSummandsN F = Multiset.foldr RootedTree.ConnesKreimer.cutForestCombinerN✝ {(0, 0)} F

@[simp]

theorem RootedTree.ConnesKreimer.cutForestSummandsN_zero {α : Type u_2} : cutForestSummandsN 0 = {(0, 0)}

@[simp]

theorem RootedTree.ConnesKreimer.cutForestSummandsN_cons {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) : cutForestSummandsN (T ::ₘ F) = Multiset.map RootedTree.ConnesKreimer.innerCombinerProj✝ (augActionN T ×ˢ cutForestSummandsN F)

Bridges to the tree-level list representation

The tree-level substrate cutListSummandsP (defined on List (RoseTree α)) is reused to evaluate cutForestSummandsN on a tree-level list rep, and to characterize cuts of a Nonplanar node. These bridges are private — the public cutSummandsN_node and comulForestN_eq_sum are stated purely at the Nonplanar level.

Tensor-algebra and multiset distributivity helpers

Public API

The two structural facts that drive the cocycle: cuts of a node decompose along cutForestSummandsN, and comulForestN expands as the multiset sum over cutForestSummandsN. Both are pure Nonplanar-level statements; tree-level substrate is invisible to consumers.

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsN_node {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : cutSummandsN (Nonplanar.node a F) = Multiset.map (fun (pf : Forest (Nonplanar α) × Forest (Nonplanar α)) => (pf.1, Nonplanar.node a pf.2)) (cutForestSummandsN F)

Cuts of Nonplanar.node a F decompose along the per-tree decisions of F: each pair (cf, rem) ∈ cutForestSummandsN F gives a cut summand (cf, Nonplanar.node a rem). The Nonplanar-level form.

theorem RootedTree.ConnesKreimer.comulForestN_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Nonplanar α)) : comulForestN F = (Multiset.map (fun (pf : Forest (Nonplanar α) × Forest (Nonplanar α)) => of' pf.1 ⊗ₜ[R] of' pf.2) (cutForestSummandsN F)).sum

The forest coproduct comulForestN F expands as a multiset sum of of' cf ⊗ of' rem over (cf, rem) ∈ cutForestSummandsN F.

The cocycle theorem (basis-level)

@[simp]

theorem RootedTree.ConnesKreimer.node_zero_eq_leaf {α : Type u_2} (a : α) : Nonplanar.node a 0 = Nonplanar.leaf a

For the empty forest: Nonplanar.node a 0 = Nonplanar.leaf a.

theorem RootedTree.ConnesKreimer.cutSummandsN_leaf {α : Type u_2} (a : α) : cutSummandsN (Nonplanar.leaf a) = {(0, Nonplanar.leaf a)}

The cut summands of a leaf: only one summand (0, leaf a), corresponding to the empty cut.

theorem RootedTree.ConnesKreimer.comulTreeN_leaf {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : comulTreeN (Nonplanar.leaf a) = ofTree (Nonplanar.leaf a) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree (Nonplanar.leaf a)

The tree-level coproduct on a leaf: comulTreeN (leaf a) = ofTree (leaf a) ⊗ 1 + 1 ⊗ ofTree (leaf a).

theorem RootedTree.ConnesKreimer.comulTreeN_node_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : comulTreeN (Nonplanar.node a F) = ofTree (Nonplanar.node a F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (Nonplanar α)) (bPlusLin a)) (comulForestN F)

The Hochschild 1-cocycle property of B+_a, on basis elements: for every forest F, the coproduct of the grafted tree Nonplanar.node a F decomposes as the explicit primitive term plus the right-channel B+ application of comulForestN F. Proven via the substrate cutSummandsN_node (cuts of a node decompose along cutForestSummandsN F) and comulForestN_eq_sum (forest coproduct expands as the matching multiset sum); the LinearMap.lTensor distributes over the sum via map_multiset_sum, and the per-summand check reduces to LinearMap.lTensor_tmul + bPlusLin_of'.

theorem RootedTree.ConnesKreimer.comulAlgHomN_bPlusLin_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : comulAlgHomN ((bPlusLin a) (of' F)) = (bPlusLin a) (of' F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (Nonplanar α)) (bPlusLin a)) (comulAlgHomN (of' F))

The cocycle, lifted to the algebra-hom level on tree basis elements.

Phase A.7-δ — Counit laws + coassoc via GL/CK duality + Bialgebra

Counit laws follow by reducing to the tree case via ConnesKreimer.algHom_ext + multiplicativity (the empty-cut summand contributes 1 ⊗ of' F; all others are killed by counit).

Coassociativity uses GL/CK duality: comulRhoN_coassoc (LinearMap form) is derived from pairing_gl_eq_pairing_coproduct_Rho (Foissy axiom) + GrossmanLarson.mul_assoc via pairing₃_unique; the AlgHom form comulAlgHomN_coassoc_algHom is a one-line lift. This replaces the earlier direct Foissy-clean proof (≈ 350 LOC, deleted in R.8 Phase 2): both Δ^ρ and Δ^c coassoc now use a single GL-duality framework.

The final Bialgebra instance is assembled via Bialgebra.ofAlgHom.

Empty cut existence (substrate for counit laws)

The empty cut (0, T) is always a cut summand of T. The tree-level substrate cutSummandsP T always contains (0, T), by mutual structural induction with cutListSummandsP; the nonplanar cutForestSummandsN F contains (0, F) by descent. These witnesses split the (counit ⊗ id) sum into a single non-vanishing summand 1 ⊗ of' F.

Tree-depth induction substrate

theorem RootedTree.ConnesKreimer.Nonplanar.depth_lt_of_mem {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) (hT : T ∈ F) (a : α) : T.depth < (Nonplanar.node a F).depth

A tree's depth is strictly less than the depth of any node containing it as a child.

Counit ⊗ id commutation with lTensor (bPlusLin a)

The factor-wise commutation (counit ⊗ id) ∘ (id ⊗ B+_a) = (id ⊗ B+_a) ∘ (counit ⊗ id) (where the right id is on different domains: H on the left, R on the right). Pure TensorProduct.induction_on calculation; both sides reduce to counit x ⊗ B+_a y on simple tensors. Used in the tree-level counit law and in the bPlus closure proof.

Symmetric: id ⊗ counit commutation with lTensor (bPlusLin a)

Mirror of counit_rTensor_lTensor_bPlus_apply. Acting on the right factor with counit and on the left factor with B+_a — they don't interact.

Tree-level counit law (depth induction)

(counit ⊗ id)(Δ T) = 1 ⊗ T for every nonplanar tree T. Strong induction on T.depth: leaves close directly via comulTreeN_leaf; nodes use the cocycle comulTreeN_node_cocycle, the commutation counit_rTensor_lTensor_bPlus_apply, and the forest law on the children.

Counit laws (algebra-hom level)

Strategy: reduce to of' F via ConnesKreimer.algHom_ext. For each F, expand comulAlgHomN (of' F) = comulForestN F via comulForestN_eq_sum, then identify the unique cut summand (0, F) ∈ cutForestSummandsN F (the "all empty cuts" tuple). Other summands have pf.1.card > 0, so counit (of' pf.1) = 0 and (counit ⊗ id) kills them. The surviving (0, F) summand contributes 1 ⊗ of' F = (lid).symm (of' F).

Helper lemmas needed (substantive):

• mem_cutSummandsN_zero (T : Nonplanar α) : (0, T) ∈ cutSummandsN T — the empty cut exists at every tree.
• cutForestSummandsN_zero_mem (F : Forest (Nonplanar α)) : (0, F) ∈ cutForestSummandsN F.
• cutForestSummandsN_pos_pi : ∀ pf ∈ cutForestSummandsN F, pf ≠ (0, F) → pf.1.card > 0.

theorem RootedTree.ConnesKreimer.counit_rTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R (Nonplanar α)))).comp comulAlgHomN = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R (Nonplanar α))).symm

theorem RootedTree.ConnesKreimer.counit_lTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (Nonplanar α))) counit).comp comulAlgHomN = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (Nonplanar α))).symm

Δ^ρ coassoc and Bialgebra instance: moved

The GL/CK duality theorem (pairing_gl_eq_pairing_coproduct_Rho), the coassociativity of comulAlgHomN, and the Bialgebra instance live in Coproduct/PruningDuality.lean, downstream of BMinus.lean (whose B⁻ calculus drives the duality proof).