Δ^ρ (admissible-cut, root-component pruning) coproduct on RootedTree.Planar α

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}

The admissible-cut, root-component pruning variant of the Connes-Kreimer coproduct on planar n-ary rooted trees. For a tree T:

Δ^ρ(T) = T ⊗ 1 + Σ_{c : Cut T} of'(cutForest c) ⊗ ofTree(remainderDeletion c)

where the empty cut contributes 1 ⊗ T (since cutForest empty = ∅).

Naming. Linglib's "Δ^ρ" corresponds to MCB Definition 1.2.6's Δ^ρ (book p. 31) — the admissible-cut coproduct whose right channel is the root component ρ_C(T) after pruning the cut subtrees from the parent's children list. The result lives in at-most-n-ary trees (Lemma 1.2.11, book p. 38). Per MCB Remark 1.2.9 (book p. 34), this Δ^ρ coproduct corresponds to the Foissy Connes-Kreimer Hopf algebra of (not-necessarily-binary) rooted trees, where the right channel can contain rooted trees that are not binary.

NOT MCB's Δ^d (Definition 1.2.5, p. 31), which is "deletion + rebinarization" — Δ^d additionally contracts edges to recover binarity. Δ^d is the closest to PF Externalization and would be derived from this Δ^ρ (or built independently) when a consumer needs it. See sibling Coproduct/Deletion.lean (FUTURE) for that.

For the trace variant Δ^c (T/^c F_v, parent arity preserved via trace leaves; MCB Definition 1.2.4, book p. 30), see sibling Coproduct/Trace.lean. MCB Δ^c on binary nonplanar = restriction of the Connes-Kreimer Hopf algebra of Feynman graphs (a different, related Hopf algebra; Remark 1.2.9, p. 34). Used at the C-I (semantic) interface for FormCopy.

Foissy clean coassoc

Δ^ρ satisfies the Hochschild 1-cocycle condition with B+ (graft as new root):

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

The B+ operator only well-defines on Multiset (Nonplanar α) → Nonplanar α (unordered children of a new root). On Planar α with Multiset forests, B+ would need a canonical ordering. Hence the sorry-free coassoc proof for Δ^ρ lives in Coproduct/PruningNonplanar.lean on RootedTree.Nonplanar α. (Note: this Foissy clean coassoc strategy does NOT generalize to Δ^c — B+ is not a Hochschild 1-cocycle for the trace variant. Δ^c coassoc uses Grossman-Larson duality instead; see the GL substrate when it lands.)

Status

[UPSTREAM] candidate. cutSummands recursive definition; full Bialgebra structure (descent + coassoc + counit + Hopf antipode) lives in Coproduct/PruningNonplanar.lean and HopfAlgebraNonplanar.lean.

cutSummandsP — multiset of (cut forest, deletion remainder) pairs

Recursive enumeration of cut summands. For a leaf, the only cut is the empty cut. For a node, sum over all per-child decisions: each child can either be extracted whole (contributes to cut forest, drops from remainder) OR recurse with a smaller cut (contributes whatever its cut extracts, leaves its deletion-remainder in the remainder list).

@[irreducible]

def RootedTree.ConnesKreimer.cutSummandsP {α : Type u_2} : Planar α → Multiset (Forest (Planar α) × Planar α)

Multiset of (cut forest, deletion remainder) pairs for a planar tree. Each summand corresponds to one admissible cut on T under the deletion semantics.

Equations

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

@[irreducible]

def RootedTree.ConnesKreimer.cutListSummandsP {α : Type u_2} : List (Planar α) → Multiset (Forest (Planar α) × List (Planar α))

Auxiliary: cut summands for a list of children. The remainder is a list (children of the parent that survived the cut).

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.ConnesKreimer.cutListSummandsP [] = {(0, [])}

@[irreducible]

def RootedTree.ConnesKreimer.augActionP {α : Type u_2} : Planar α → Multiset (Forest (Planar α) × Option (Planar α))

Auxiliary: per-child action — either extract whole (none remainder) or recurse with a cut (some remainder).

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsP_node {α : Type u_2} (a : α) (cs : List (Planar α)) : cutSummandsP (Planar.node a cs) = Multiset.map (fun (p : Forest (Planar α) × List (Planar α)) => (p.1, Planar.node a p.2)) (cutListSummandsP cs)

Recursive formula on a node: cutSummandsP unfolds via cutListSummandsP.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsP_nil {α : Type u_2} : cutListSummandsP [] = {(0, [])}

Recursive formula for cutListSummandsP on empty list.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsP_cons {α : Type u_2} (t : Planar α) (ts : List (Planar α)) : cutListSummandsP (t :: ts) = Multiset.map (fun (p : (Forest (Planar α) × Option (Planar α)) × Forest (Planar α) × List (Planar α)) => match p.1.2 with | none => (p.1.1 + p.2.1, p.2.2) | some r => (p.1.1 + p.2.1, r :: p.2.2)) (augActionP t ×ˢ cutListSummandsP ts)

Recursive formula for cutListSummandsP on a cons list.

@[simp]

theorem RootedTree.ConnesKreimer.augActionP_eq {α : Type u_2} (t : Planar α) : augActionP t = ({t}, none) ::ₘ Multiset.map (fun (p : Forest (Planar α) × Planar α) => (p.1, some p.2)) (cutSummandsP t)

Recursive formula for augActionP.

comulTreePlanarP — tree-level Δ^ρ

Sum the cut summands as tensors, plus the explicit T ⊗ 1 term.

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

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

Equations

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

comulForestPlanarP — forest-level Δ^ρ

Multiplicative extension over the disjoint-union product on forests: Δ(F + G) = Δ(F) · Δ(G).

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

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

Equations

• RootedTree.ConnesKreimer.comulForestPlanarP F = (Multiset.map RootedTree.ConnesKreimer.comulTreePlanarP F).prod

@[simp]

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

@[simp]

theorem RootedTree.ConnesKreimer.comulForestPlanarP_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Planar α)) : comulForestPlanarP (F + G) = comulForestPlanarP F * comulForestPlanarP G

comulMonoidHom and comulAlgHom

Package the multiplicative extension as a MonoidHom, then lift to the full AlgHom via AddMonoidAlgebra.lift.

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

comulForestPlanarP as a monoid hom from Multiplicative (Forest (Planar α)).

Equations

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

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

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

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomP_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Planar α)) : comulAlgHomP (of' F) = comulForestPlanarP F

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomP_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Planar α) : comulAlgHomP (ofTree T) = comulTreePlanarP T