Connes–Kreimer / Foissy (planar, R1) coproduct as a genuine Mathlib Coalgebra instance. Combinatorial core (List.Perm) proven below verbatim from Coassoc.lean; the Mathlib bridge lifts it to equality of linear maps. LOCAL — not part of the published godsil tree.

inductive CK.RTree : Type

Planar rooted trees, represented by the forest of children below the root.

• node : List RTree → RTree

@[implicit_reducible]

instance CK.instInhabitedRTree : Inhabited RTree

Equations

• CK.instInhabitedRTree = { default := CK.instInhabitedRTree.default }

@[reducible, inline]

abbrev CK.Forest : Type

A planar rooted forest is a list of planar rooted trees.

Equations

• CK.Forest = List CK.RTree

@[reducible, inline]

abbrev CK.Tens : Type

Formal sums of coproduct tensor monomials, represented by their forest pairs.

Equations

• CK.Tens = List (CK.Forest × CK.Forest)

def CK.tmul (x y : Tens) : Tens

Product on formal tensor monomials, multiplying the two tensor legs by forest concatenation.

Equations

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

def CK.coprodTree : RTree → Tens

The Connes-Kreimer coproduct on one rooted tree, as a formal list of tensor terms.

Equations

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

def CK.coprodForest : Forest → Tens

The multiplicative extension of the coproduct from trees to forests.

Equations

• CK.coprodForest [] = [([], [])]
• CK.coprodForest (t :: ts) = CK.tmul (CK.coprodTree t) (CK.coprodForest ts)

@[simp]

theorem CK.tmul_unit_left (y : Tens) : tmul [([], [])] y = y

@[simp]

theorem CK.tmul_unit_right (x : Tens) : tmul x [([], [])] = x

theorem CK.tmul_append_left (x₁ x₂ y : Tens) : tmul (x₁ ++ x₂) y = tmul x₁ y ++ tmul x₂ y

theorem CK.tmul_cons (p r : Forest) (xs y : Tens) : tmul ((p, r) :: xs) y = List.map (fun (x : Forest × Forest) => match x with | (p', r') => (p ++ p', r ++ r')) y ++ tmul xs y

theorem CK.tmul_assoc (x y z : Tens) : tmul (tmul x y) z = tmul x (tmul y z)

theorem CK.coprodForest_append (F G : Forest) : coprodForest (F ++ G) = tmul (coprodForest F) (coprodForest G)

theorem CK.perm_middle_swap {α : Type u_1} (A B C D : List α) : (A ++ B ++ (C ++ D)).Perm (A ++ C ++ (B ++ D))

theorem CK.flatMap_append_distrib {α : Type u_1} {β : Type u_2} (l : List α) (X Y : α → List β) : (List.flatMap (fun (a : α) => X a ++ Y a) l).Perm (List.flatMap X l ++ List.flatMap Y l)

theorem CK.flatMap_const_nil {α : Type u_1} {β : Type u_2} (l : List α) : List.flatMap (fun (x : α) => []) l = []

theorem CK.flatMap_singleton_eq_map {α : Type u_1} {β : Type u_2} (g : α → β) (l : List α) : List.flatMap (fun (a : α) => [g a]) l = List.map g l

theorem CK.flatMap_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l1 : List α) (l2 : List β) (f : α → β → List γ) : (List.flatMap (fun (a : α) => List.flatMap (fun (b : β) => f a b) l2) l1).Perm (List.flatMap (fun (b : β) => List.flatMap (fun (a : α) => f a b) l1) l2)

theorem CK.Perm.flatMap_congr_right {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β} (h : ∀ (a : α), (f a).Perm (g a)) : (List.flatMap f l).Perm (List.flatMap g l)

@[reducible, inline]

abbrev CK.Tens3 : Type

Formal sums of triple tensor monomials, represented by forest triples.

Equations

• CK.Tens3 = List (CK.Forest × CK.Forest × CK.Forest)

def CK.coLeft (x : Tens) : Tens3

Expand the left tensor leg of every coproduct term.

Equations

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

def CK.coRight (x : Tens) : Tens3

Expand the right tensor leg of every coproduct term.

Equations

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

def CK.tmul3 (x y : Tens3) : Tens3

Product on formal triple tensor monomials, multiplying all three tensor legs.

Equations

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

theorem CK.coLeft_tmul (x y : Tens) : List.Perm (coLeft (tmul x y)) (tmul3 (coLeft x) (coLeft y))

theorem CK.coRight_tmul (x y : Tens) : List.Perm (coRight (tmul x y)) (tmul3 (coRight x) (coRight y))

theorem CK.coprodTree_node (F : Forest) : coprodTree (RTree.node F) = ([RTree.node F], []) :: List.map (fun (pr : Forest × Forest) => (pr.1, [RTree.node pr.2])) (coprodForest F)

theorem CK.coprodForest_single (t : RTree) : coprodForest [t] = coprodTree t

theorem CK.tmul3_perm {a a' b b' : Tens3} (ha : List.Perm a a') (hb : List.Perm b b') : List.Perm (tmul3 a b) (tmul3 a' b')

theorem CK.coassocTree (t : RTree) : List.Perm (coLeft (coprodTree t)) (coRight (coprodTree t))

theorem CK.coassocForest (F : Forest) : List.Perm (coLeft (coprodForest F)) (coRight (coprodForest F))

Mathlib bridge: lift the combinatorial coassoc to a Coalgebra instance.

@[reducible, inline]

abbrev CK.H (k : Type u_1) [CommRing k] : Type u_1

Carrier: forests with k-coefficients (product = forest concatenation).

Equations

• CK.H k = MonoidAlgebra k (FreeMonoid CK.RTree)

noncomputable def CK.e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : TensorProduct k (H k) (H k)

Pure 2-tensor of a cut (p, r).

Equations

• CK.e2 k pr = MonoidAlgebra.single pr.1 1 ⊗ₜ[k] MonoidAlgebra.single pr.2 1

noncomputable def CK.e3 (k : Type u_1) [CommRing k] (t : Forest × Forest × Forest) : TensorProduct k (H k) (TensorProduct k (H k) (H k))

Pure 3-tensor of an iterated cut (a, b, c), associated to the right.

Equations

• CK.e3 k t = MonoidAlgebra.single t.1 1 ⊗ₜ[k] (MonoidAlgebra.single t.2.1 1 ⊗ₜ[k] MonoidAlgebra.single t.2.2 1)

noncomputable def CK.Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : TensorProduct k (H k) (H k)

Δ on a basis forest.

Equations

• CK.Δ₀ k f = (List.map (CK.e2 k) (CK.coprodForest f)).sum

noncomputable def CK.E3 (k : Type u_1) [CommRing k] (l : Tens3) : TensorProduct k (H k) (TensorProduct k (H k) (H k))

E3 of a triple-tensor list.

Equations

• CK.E3 k l = (List.map (CK.e3 k) l).sum

noncomputable def CK.Δ (k : Type u_1) [CommRing k] : H k →ₗ[k] TensorProduct k (H k) (H k)

Comultiplication.

Equations

• CK.Δ k = Finsupp.linearCombination k (CK.Δ₀ k)

theorem CK.Δ_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (Δ k) (MonoidAlgebra.single f b) = b • Δ₀ k f

theorem CK.E3_flatMap (k : Type u_1) [CommRing k] (L : Tens) (g : Forest × Forest → Tens3) : E3 k (List.flatMap g L) = (List.map (fun (x : Forest × Forest) => E3 k (g x)) L).sum

E3 distributes over flatMap.

theorem CK.linmap_list_sum (k : Type u_1) [CommRing k] {α : Type u_4} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] (φ : M →ₗ[k] N) (l : List α) (h : α → M) : φ (List.map h l).sum = (List.map (fun (a : α) => φ (h a)) l).sum

A linear map commutes with a List.sum of mapped terms.

theorem CK.elem_lemma (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (TensorProduct.assoc k (H k) (H k) (H k)) ((LinearMap.rTensor (H k) (Δ k)) (e2 k pr)) = E3 k (List.map (fun (ab : Forest × Forest) => (ab.1, ab.2, pr.2)) (coprodForest pr.1))

The per-cut computation: assoc ∘ rTensor Δ on a pure 2-tensor e2 (p,r) equals E3 of the left-leg refinement. This is the heart of the coassoc bridge.

theorem CK.elem_lemma_R (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.lTensor (H k) (Δ k)) (e2 k pr) = E3 k (List.map (fun (bc : Forest × Forest) => (pr.1, bc.1, bc.2)) (coprodForest pr.2))

Right-leg analogue: lTensor Δ on e2 (p,r) equals E3 of the right-leg refinement. No assoc needed — the tensor is already right-associated.

theorem CK.lhs_core (k : Type u_1) [CommRing k] (f : Forest) : (TensorProduct.assoc k (H k) (H k) (H k)) ((LinearMap.rTensor (H k) (Δ k)) (Δ₀ k f)) = E3 k (coLeft (coprodForest f))

LHS structural map on Δ₀ f.

theorem CK.rhs_core (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.lTensor (H k) (Δ k)) (Δ₀ k f) = E3 k (coRight (coprodForest f))

RHS structural map on Δ₀ f.

theorem CK.perm_E3 (k : Type u_1) [CommRing k] (f : Forest) : E3 k (coLeft (coprodForest f)) = E3 k (coRight (coprodForest f))

The combinatorial coassoc, transported to E3.

theorem CK.coassoc_map (k : Type u_1) [CommRing k] : ↑(TensorProduct.assoc k (H k) (H k) (H k)) ∘ₗ LinearMap.rTensor (H k) (Δ k) ∘ₗ Δ k = LinearMap.lTensor (H k) (Δ k) ∘ₗ Δ k

Coassociativity as an equality of linear maps.

Counit.

def CK.εmon (k : Type u_1) [CommRing k] : FreeMonoid RTree →* k

Counit monoid hom: every generator ↦ 0, so a word ↦ 0 ^ len = indicator of empty.

Equations

• CK.εmon k = FreeMonoid.lift fun (x : CK.RTree) => 0

@[simp]

theorem CK.εmon_nil (k : Type u_1) [CommRing k] : (εmon k) [] = 1

@[simp]

theorem CK.εmon_of (k : Type u_1) [CommRing k] (a : RTree) : (εmon k) (FreeMonoid.of a) = 0

@[simp]

theorem CK.εmon_cons (k : Type u_1) [CommRing k] (a : RTree) (l : Forest) : (εmon k) (a :: l) = 0

theorem CK.εmon_append (k : Type u_1) [CommRing k] (p p' : Forest) : (εmon k) (p ++ p') = (εmon k) p * (εmon k) p'

noncomputable def CK.εalg (k : Type u_1) [CommRing k] : H k →ₐ[k] k

Counit as an algebra hom, then linear.

Equations

• CK.εalg k = (MonoidAlgebra.lift k k (FreeMonoid CK.RTree)) (CK.εmon k)

noncomputable def CK.ε (k : Type u_1) [CommRing k] : H k →ₗ[k] k

The Connes-Kreimer counit as a linear map.

Equations

• CK.ε k = (CK.εalg k).toLinearMap

theorem CK.ε_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (ε k) (MonoidAlgebra.single f b) = b * (εmon k) f

theorem CK.smul_list_sum (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (c : k) (l : List M) : c • l.sum = (List.map (fun (x : M) => c • x) l).sum

Scalar smul commutes with a List.sum.

theorem CK.smul_list_sum' (k : Type u_1) [CommRing k] {α : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module k M] (c : k) (l : List α) (F : α → M) : c • (List.map F l).sum = (List.map (fun (x : α) => c • F x) l).sum

Smul through a mapped List.sum.

theorem CK.tmul_scalar_right (k : Type u_1) [CommRing k] (m : H k) (c : k) : m ⊗ₜ[k] c = c • m ⊗ₜ[k] 1

Pull a base-ring scalar out of the right tensor leg (avoids CompatibleSMul).

theorem CK.tmul_scalar_left (k : Type u_1) [CommRing k] (c : k) (m : H k) : c ⊗ₜ[k] m = c • 1 ⊗ₜ[k] m

Pull a base-ring scalar out of the left tensor leg.

theorem CK.map_flatMap_sum {α : Type u_2} {β : Type u_3} {M : Type u_4} [AddCommMonoid M] (L : List α) (G : α → List β) (h : β → M) : (List.map h (List.flatMap G L)).sum = (List.map (fun (a : α) => (List.map h (G a)).sum) L).sum

Generic map-over-flatMap List.sum distribution.

The left-counit collapse: ε on the left leg selects the unique ([], f) cut.

theorem CK.collapseL_tree (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (t : RTree) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.1 • g pr.2) (coprodTree t)).sum = g [t]

theorem CK.collapseL_forest (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (f : Forest) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.1 • g pr.2) (coprodForest f)).sum = g f

The right-counit collapse: ε on the right leg selects the unique (f, []) cut.

theorem CK.collapseR_tree (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (t : RTree) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.2 • g pr.1) (coprodTree t)).sum = g [t]

theorem CK.collapseR_forest (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (f : Forest) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.2 • g pr.1) (coprodForest f)).sum = g f

theorem CK.rTensor_ε_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.rTensor (H k) (ε k)) (Δ₀ k f) = 1 ⊗ₜ[k] MonoidAlgebra.single f 1

(ε ⊗ id) ∘ Δ on a basis forest gives 1 ⊗ single f 1.

theorem CK.lTensor_ε_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.lTensor (H k) (ε k)) (Δ₀ k f) = MonoidAlgebra.single f 1 ⊗ₜ[k] 1

(id ⊗ ε) ∘ Δ on a basis forest gives single f 1 ⊗ 1.

theorem CK.single_smul_one (k : Type u_1) [CommRing k] (f : FreeMonoid RTree) (b : k) : MonoidAlgebra.single f b = b • MonoidAlgebra.single f 1

@[implicit_reducible]

noncomputable instance CK.instCoalgebraStructH (k : Type u_1) [CommRing k] : CoalgebraStruct k (H k)

Equations

• CK.instCoalgebraStructH k = { comul := CK.Δ k, counit := CK.ε k }

@[implicit_reducible]

noncomputable instance CK.instCKCoalg (k : Type u_1) [CommRing k] : Coalgebra k (H k)

Equations

• CK.instCKCoalg k = { toCoalgebraStruct := CK.instCoalgebraStructH k, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

Bialgebra: Δ and ε are algebra homs.

theorem CK.single_append (k : Type u_1) [CommRing k] (p p' : Forest) : MonoidAlgebra.single (p ++ p') 1 = MonoidAlgebra.single p 1 * MonoidAlgebra.single p' 1

single of a concatenation is the product (algebra structure of H).

theorem CK.e2_mul (k : Type u_1) [CommRing k] (pr pr' : Forest × Forest) : e2 k (pr.1 ++ pr'.1, pr.2 ++ pr'.2) = e2 k pr * e2 k pr'

e2 is multiplicative across leg-wise concatenation.

theorem CK.mul_list_sum {M : Type u_2} [NonUnitalNonAssocSemiring M] (a : M) (L : List M) : a * L.sum = (List.map (fun (b : M) => a * b) L).sum

Left-distribute a product over a List.sum.

theorem CK.list_sum_mul_sum {M : Type u_2} [NonUnitalNonAssocSemiring M] (L1 L2 : List M) : L1.sum * L2.sum = (List.flatMap (fun (a : M) => List.map (fun (b : M) => a * b) L2) L1).sum

Product of two List.sums is the double sum.

theorem CK.Δ₀_mul (k : Type u_1) [CommRing k] (F G : Forest) : Δ₀ k (F ++ G) = Δ₀ k F * Δ₀ k G

Δ₀ is multiplicative.

theorem CK.Δ_mul (k : Type u_1) [CommRing k] (a b : H k) : (Δ k) (a * b) = (Δ k) a * (Δ k) b

Δ is multiplicative on all of H (reduce to the forest basis, bilinearly).

theorem CK.Δ_one (k : Type u_1) [CommRing k] : (Δ k) 1 = 1

Δ 1 = 1.

@[implicit_reducible]

noncomputable instance CK.instCKBialg (k : Type u_1) [CommRing k] : Bialgebra k (H k)

Equations

• CK.instCKBialg k = Bialgebra.mk' k (CK.H k) ⋯ ⋯ ⋯ ⋯

Toward HopfAlgebra: node count (grading) and its conservation under cuts.

Conservation `|p| + |r| = |f|` makes the antipode recursion well-founded
(`r ≠ [] ⟹ |p| < |f|`). 

def CK.sizeT : RTree → ℕ

Number of nodes in a rooted tree.

Equations

• CK.sizeT (CK.RTree.node F) = 1 + CK.sizeF F

def CK.sizeF : Forest → ℕ

Number of nodes in a rooted forest.

Equations

• CK.sizeF [] = 0
• CK.sizeF (t :: ts) = CK.sizeT t + CK.sizeF ts

theorem CK.sizeF_append (F G : Forest) : sizeF (F ++ G) = sizeF F + sizeF G

theorem CK.size_consTree (t : RTree) (pr : Forest × Forest) : pr ∈ coprodTree t → sizeF pr.1 + sizeF pr.2 = sizeT t

theorem CK.size_consForest (f : Forest) (pr : Forest × Forest) : pr ∈ coprodForest f → sizeF pr.1 + sizeF pr.2 = sizeF f

theorem CK.sizeF_pos {f : Forest} (h : f ≠ []) : 0 < sizeF f

noncomputable def CK.sf (k : Type u_1) [CommRing k] (r : Forest) : H k

A forest as an H-basis element, with the index forced to FreeMonoid RTree via ofList (so it is always typed H k, even on the empty forest).

Equations

• CK.sf k r = MonoidAlgebra.single (FreeMonoid.ofList r) 1

@[simp]

theorem CK.sf_nil (k : Type u_1) [CommRing k] : sf k [] = 1

theorem CK.sf_append (k : Type u_1) [CommRing k] (a b : Forest) : sf k (a ++ b) = sf k a * sf k b

@[irreducible]

noncomputable def CK.antipodeF (k : Type u_1) [CommRing k] : Forest → H k

The antipode on the forest basis, by well-founded recursion on node count. S(∅) = 1; S(f) = -Σ_{(p,r) cut, r ≠ ∅} S(p)·r. Recursion decreases since |p| < |f|.

Equations

• One or more equations did not get rendered due to their size.
• CK.antipodeF k [] = 1

Antipode as a linear map + the left convolution axiom (S ⋆ id = η∘ε).

noncomputable def CK.antipode (k : Type u_1) [CommRing k] : H k →ₗ[k] H k

The antipode linear map obtained by extending antipodeF from the forest basis.

Equations

• CK.antipode k = Finsupp.linearCombination k (CK.antipodeF k)

theorem CK.antipode_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (antipode k) (MonoidAlgebra.single f b) = b • antipodeF k f

theorem CK.antipodeF_cons (k : Type u_1) [CommRing k] (t : RTree) (ts : Forest) : antipodeF k (t :: ts) = -(List.map (fun (pr : Forest × Forest) => antipodeF k pr.1 * sf k pr.2) (List.filter (fun (pr : Forest × Forest) => !List.isEmpty pr.2) (coprodForest (t :: ts)))).sum

antipodeF on a nonempty forest, as a plain (non-attach) sum.

theorem CK.isEmpty_append_of_ne {r b : Forest} (h : r ≠ []) : List.isEmpty (r ++ b) = false

r ++ b is nonempty when r is.

theorem CK.filter_emptyR_tmul (A B : Tens) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (tmul A B) = tmul (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) A) (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) B)

Filtering cuts by "empty right leg" factorizes over tmul.

theorem CK.coprodTree_filter_emptyR (t : RTree) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (coprodTree t) = [([t], [])]

The unique empty-right cut of a tree t is ([t], []).

theorem CK.coprodForest_filter_emptyR (f : Forest) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (coprodForest f) = [(f, [])]

theorem CK.filter_emptyL_tmul (A B : Tens) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (tmul A B) = tmul (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) A) (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) B)

Filtering cuts by "empty left leg" factorizes over tmul.

theorem CK.coprodTree_filter_emptyL (t : RTree) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (coprodTree t) = [([], [t])]

The unique empty-left cut of a tree t is ([], [t]).

theorem CK.coprodForest_filter_emptyL (f : Forest) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (coprodForest f) = [([], f)]

theorem CK.map_sum_filter_split (k : Type u_1) [CommRing k] {α : Type u_2} (L : List α) (P : α → Bool) (g : α → H k) : (List.map g L).sum = (List.map g (List.filter P L)).sum + (List.map g (List.filter (fun (x : α) => !P x) L)).sum

Split a mapped List.sum by a boolean predicate.

theorem CK.leftConvF (k : Type u_1) [CommRing k] (f : Forest) : (List.map (fun (pr : Forest × Forest) => antipodeF k pr.1 * sf k pr.2) (coprodForest f)).sum = (εmon k) f • 1

Left convolution axiom on a basis forest: (S ⋆ id)(f) = ε(f)·1. Near-definitional.

theorem CK.mul_rTensor_antipode_e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((LinearMap.rTensor (H k) (antipode k)) (e2 k pr)) = antipodeF k pr.1 * sf k pr.2

μ ∘ (S ⊗ id) on a pure 2-tensor e2 (p,r) gives S(p)·r.

theorem CK.rTensor_antipode_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.mul' k (H k) ∘ₗ LinearMap.rTensor (H k) (antipode k)) (Δ₀ k f) = (εmon k) f • 1

μ ∘ (S ⊗ id) ∘ Δ on a basis forest equals ε(f)·1 (left antipode identity).

Mirror (right) antipode S', satisfying id ⋆ S' = η∘ε.

@[irreducible]

noncomputable def CK.antipodeF' (k : Type u_1) [CommRing k] : Forest → H k

The right antipode by well-founded recursion on node count. S'(∅) = 1; S'(f) = -Σ_{(p,r) cut, p ≠ ∅} p·S'(r). Decreases since |r| < |f|.

Equations

• One or more equations did not get rendered due to their size.
• CK.antipodeF' k [] = 1

theorem CK.antipodeF'_cons (k : Type u_1) [CommRing k] (t : RTree) (ts : Forest) : antipodeF' k (t :: ts) = -(List.map (fun (pr : Forest × Forest) => sf k pr.1 * antipodeF' k pr.2) (List.filter (fun (pr : Forest × Forest) => !List.isEmpty pr.1) (coprodForest (t :: ts)))).sum

theorem CK.rightConvF' (k : Type u_1) [CommRing k] (f : Forest) : (List.map (fun (pr : Forest × Forest) => sf k pr.1 * antipodeF' k pr.2) (coprodForest f)).sum = (εmon k) f • 1

Right convolution id ⋆ S' on a basis forest equals ε(f)·1. Near-definitional.

noncomputable def CK.antipode' (k : Type u_1) [CommRing k] : H k →ₗ[k] H k

The mirrored antipode candidate used to prove the right convolution identity.

Equations

• CK.antipode' k = Finsupp.linearCombination k (CK.antipodeF' k)

theorem CK.antipode'_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (antipode' k) (MonoidAlgebra.single f b) = b • antipodeF' k f

theorem CK.mul_lTensor_antipode'_e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((LinearMap.lTensor (H k) (antipode' k)) (e2 k pr)) = sf k pr.1 * antipodeF' k pr.2

theorem CK.lTensor_antipode'_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode' k)) (Δ₀ k f) = (εmon k) f • 1

μ ∘ (id ⊗ S') ∘ Δ on a basis forest equals ε(f)·1 (right antipode identity).

theorem CK.leftAntipode_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.rTensor (H k) (antipode k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

Left antipode identity as a linear-map equality (the Hopf left axiom).

theorem CK.rightAntipode'_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode' k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

Right antipode identity for S' as a linear-map equality.

theorem CK.antipode_eq_antipode' (k : Type u_1) [CommRing k] : antipode k = antipode' k

The left and right antipodes coincide (a left convolution-inverse of id that has a right convolution-inverse must equal it — pure monoid algebra in WithConv).

@[implicit_reducible]

noncomputable instance CK.instHopfAlgebraStructH (k : Type u_1) [CommRing k] : HopfAlgebraStruct k (H k)

Equations

• CK.instHopfAlgebraStructH k = { toBialgebra := CK.instCKBialg k, antipode := CK.antipode k }

@[implicit_reducible]

noncomputable instance CK.instCKHopf (k : Type u_1) [CommRing k] : HopfAlgebra k (H k)

Equations

• CK.instCKHopf k = { toHopfAlgebraStruct := CK.instHopfAlgebraStructH k, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

Adams operators Ψₙ = id^{⋆n} and the antipode as Ψ₋₁.

The convolution ring `WithConv (H k →ₗ[k] H k)` (Mathlib `LinearMap.convRing`) turns the
identity into a ring element whose convolution powers are the Adams (Hopf-power) operators.
`Ψ₀ = u∘ε` (the convolution unit), `Ψ₁ = id`, the semigroup law `Ψₘ ⋆ Ψₙ = Ψₘ₊ₙ`, and the
identity is a convolution UNIT whose inverse is the antipode — i.e. `Ψ₋₁ = S`. This is the
first combinatorial-Hopf Adams-operator layer in any ITP (Aguiar–Lauve theory; the Eulerian
idempotent `e⁽¹⁾ = log_⋆ id` is the heavier next step, needing connected-graded nilpotence). 

noncomputable def CK.adams (k : Type u_1) [CommRing k] (n : ℕ) : H k →ₗ[k] H k

The n-th Adams operator Ψₙ = id^{⋆n}: the n-th convolution power of the identity in the convolution ring WithConv (H k →ₗ[k] H k).

Equations

• CK.adams k n = (WithConv.toConv LinearMap.id ^ n).ofConv

theorem CK.toConv_adams (k : Type u_1) [CommRing k] (n : ℕ) : WithConv.toConv (adams k n) = WithConv.toConv LinearMap.id ^ n

@[simp]

theorem CK.toConv_adams_zero (k : Type u_1) [CommRing k] : WithConv.toConv (adams k 0) = 1

Ψ₀ = u∘ε is the convolution unit.

@[simp]

theorem CK.adams_one (k : Type u_1) [CommRing k] : adams k 1 = LinearMap.id

Ψ₁ = id.

theorem CK.toConv_adams_add (k : Type u_1) [CommRing k] (m n : ℕ) : WithConv.toConv (adams k (m + n)) = WithConv.toConv (adams k m) * WithConv.toConv (adams k n)

The convolution-power semigroup law Ψₘ ⋆ Ψₙ = Ψₘ₊ₙ.

theorem CK.antipode_convMul_id (k : Type u_1) [CommRing k] : WithConv.toConv (antipode k) * WithConv.toConv LinearMap.id = 1

S ⋆ id = u∘ε: the antipode is a left convolution inverse of Ψ₁ = id.

theorem CK.id_convMul_antipode (k : Type u_1) [CommRing k] : WithConv.toConv LinearMap.id * WithConv.toConv (antipode k) = 1

id ⋆ S = u∘ε: the antipode is also a right convolution inverse of Ψ₁ = id.

noncomputable def CK.adamsUnit (k : Type u_1) [CommRing k] : (WithConv (H k →ₗ[k] H k))ˣ

Ψ₁ = id is a convolution UNIT, with the antipode as its (two-sided) inverse. This is the precise sense in which Ψ₋₁ = S.

Equations

• CK.adamsUnit k = { val := WithConv.toConv LinearMap.id, inv := WithConv.toConv (CK.antipode k), val_inv := ⋯, inv_val := ⋯ }

theorem CK.adamsUnit_inv_val (k : Type u_1) [CommRing k] : ↑(adamsUnit k)⁻¹ = WithConv.toConv (antipode k)

Ψ₋₁ = S: the inverse of the Adams unit Ψ₁ is the antipode.

Part 2 — local nilpotency of J = id − u∘ε (the connected-graded engine for log_⋆).

`J` kills the empty forest and is the identity on nonempty ones. Its convolution powers
`J^{⋆k}` vanish on every basis forest of fewer than `k` nodes (`Jc_pow_ofConv_sf_eq_zero`):
each of the `k` convolution factors must absorb at least one node, so `k` nodes are needed.
Hence the series `log_⋆(id) = Σ_{k≥1} ((-1)^{k+1}/k)·J^{⋆k}` is finite in each degree — the
connected-graded local nilpotency on which the Aguiar–Lauve Eulerian spectrum rests. 

theorem CK.Δ_sf (k : Type u_1) [CommRing k] (f : Forest) : (Δ k) (sf k f) = Δ₀ k f

Δ on a basis forest, packaged for sf.

theorem CK.ε_sf (k : Type u_1) [CommRing k] (p : Forest) : (ε k) (sf k p) = (εmon k) p

ε on a basis forest: the counit of sf f is εmon f.

theorem CK.mul_map_e2 (k : Type u_1) [CommRing k] (F G : H k →ₗ[k] H k) (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((TensorProduct.map F G) (e2 k pr)) = F (sf k pr.1) * G (sf k pr.2)

μ ∘ (F ⊗ G) on a pure cut-tensor e2 (p,r) is F(p)·G(r).

theorem CK.comul_sf (k : Type u_1) [CommRing k] (f : Forest) : CoalgebraStruct.comul (sf k f) = Δ₀ k f

comul on a basis forest equals the combinatorial Δ₀.

theorem CK.conv_ofConv_sf (k : Type u_1) [CommRing k] (F G : H k →ₗ[k] H k) (f : Forest) : (WithConv.toConv F * WithConv.toConv G).ofConv (sf k f) = (List.map (fun (pr : Forest × Forest) => F (sf k pr.1) * G (sf k pr.2)) (coprodForest f)).sum

Convolution-on-basis engine. (F ⋆ G) on a basis forest is the sum over cuts: (F ⋆ G)(f) = Σ_{(p,r) ∈ coprodForest f} F(p)·G(r). Reusable for all of Part 2.

noncomputable def CK.Jc (k : Type u_1) [CommRing k] : WithConv (H k →ₗ[k] H k)

The augmentation projector J = id − u∘ε, as an element of the convolution ring.

Equations

• CK.Jc k = WithConv.toConv LinearMap.id - 1

theorem CK.convOne_ofConv_sf (k : Type u_1) [CommRing k] (p : Forest) : (WithConv.ofConv 1) (sf k p) = (εmon k) p • 1

The convolution unit 1 = u∘ε on a basis forest: ε(f)·1.

theorem CK.Jc_ofConv_sf (k : Type u_1) [CommRing k] (p : Forest) : (Jc k).ofConv (sf k p) = sf k p - (εmon k) p • 1

J = id − u∘ε on a basis forest: kills the empty forest, identity otherwise.

theorem CK.Jc_pow_ofConv_sf_eq_zero (k : Type u_1) [CommRing k] (n : ℕ) (f : Forest) : sizeF f < n → (Jc k ^ n).ofConv (sf k f) = 0

Local nilpotency. J^{⋆n} = (id − u∘ε)^{⋆n} vanishes on every basis forest with fewer than n nodes. Proof: induction on n via the convolution engine and degree conservation; in a nonzero cut the left leg carries ≥1 node, so the right leg has < n−1 nodes and the induction hypothesis kills it, while an empty left leg is killed by J directly.

The Adams eigenvalue on primitives: Ψₙ(x) = n·x for primitive x.

The first piece of the Aguiar–Lauve spectrum, valid on ANY connected graded bialgebra (no
commutativity needed): the primitives are the eigenspace of every Adams operator `Ψₙ` with
eigenvalue `n`. Proof is at the element level (not the basis): on a primitive `x`, the recursion
`Ψₙ₊₁ = id ⋆ Ψₙ` and `Δx = x⊗1 + 1⊗x` give `Ψₙ₊₁(x) = x + Ψₙ(x)`, and `Ψₙ` fixes the unit. 

def CK.IsPrimitive (k : Type u_1) [CommRing k] (x : H k) : Prop

A primitive element: Δx = x⊗1 + 1⊗x.

Equations

• CK.IsPrimitive k x = ((CK.Δ k) x = x ⊗ₜ[k] 1 + 1 ⊗ₜ[k] x)

theorem CK.conv_apply (k : Type u_1) [CommRing k] (F G : H k →ₗ[k] H k) (x : H k) : (WithConv.toConv F * WithConv.toConv G).ofConv x = (LinearMap.mul' k (H k)) ((TensorProduct.map F G) ((Δ k) x))

Convolution at the element level: (F ⋆ G)(x) = μ((F⊗G)(Δx)).

theorem CK.Δ_one_tmul (k : Type u_1) [CommRing k] : (Δ k) 1 = 1 ⊗ₜ[k] 1

Δ(1) = 1⊗1 (the unit is grouplike), in pure-tensor form.

theorem CK.adams_succ_apply (k : Type u_1) [CommRing k] (n : ℕ) (x : H k) : (adams k (n + 1)) x = (LinearMap.mul' k (H k)) ((TensorProduct.map LinearMap.id (adams k n)) ((Δ k) x))

Ψₙ₊₁ = id ⋆ Ψₙ evaluated: Ψₙ₊₁(x) = μ((id⊗Ψₙ)(Δx)).

theorem CK.adams_unit (k : Type u_1) [CommRing k] (n : ℕ) : (adams k n) 1 = 1

Every Adams operator fixes the unit: Ψₙ(1) = 1.

theorem CK.adams_primitive (k : Type u_1) [CommRing k] (n : ℕ) {x : H k} (hx : IsPrimitive k x) : (adams k (n + 1)) x = (n + 1) • x

Adams eigenvalue on primitives: for primitive x, Ψₙ₊₁(x) = (n+1)·x. The primitives are the eigenspace of Ψₙ with eigenvalue n, and S = Ψ₋₁ acts as −1, recovering S(x) = −x.

The first Eulerian idempotent e⁽¹⁾ = log_⋆(id) as a linear map.

Over a `ℚ`-algebra the series `log_⋆(id) = Σ_{k≥1} ((-1)^{k+1}/k)·J^{⋆k}` is, by the local
nilpotency above, finite on each basis forest (only `k ≤ |f|` contribute). We define `e⁽¹⁾`
by that finite per-degree sum, mirroring how `Δ` and the antipode are defined on the basis.
`e⁽¹⁾` kills the unit and fixes primitives (eigenvalue `1`) — the connected-graded projector
onto primitives that begins the Aguiar–Lauve spectral decomposition. 

noncomputable def CK.eulerCoef (k : Type u_1) [CommRing k] [Algebra ℚ k] (j : ℕ) : k

Coefficient (-1)^{j+1}/j of the convolution-log series, pushed into k. j = 0 ↦ 0.

Equations

• CK.eulerCoef k j = (algebraMap ℚ k) ((-1) ^ (j + 1) / ↑j)

@[simp]

theorem CK.eulerCoef_zero (k : Type u_1) [CommRing k] [Algebra ℚ k] : eulerCoef k 0 = 0

@[simp]

theorem CK.eulerCoef_one (k : Type u_1) [CommRing k] [Algebra ℚ k] : eulerCoef k 1 = 1

noncomputable def CK.eulerian1F (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) : H k

e⁽¹⁾ on a basis forest: the finite log series Σ_{j=0}^{|f|} ((-1)^{j+1}/j)·J^{⋆j}(f) (the j=0 term is 0; terms with j > |f| are absent — and would vanish anyway).

Equations

• CK.eulerian1F k f = (List.map (fun (j : ℕ) => CK.eulerCoef k j • (CK.Jc k ^ j).ofConv (CK.sf k f)) (List.range (CK.sizeF f + 1))).sum

noncomputable def CK.eulerian1 (k : Type u_1) [CommRing k] [Algebra ℚ k] : H k →ₗ[k] H k

The first Eulerian idempotent e⁽¹⁾ : H → H, linear extension of eulerian1F.

Equations

• CK.eulerian1 k = Finsupp.linearCombination k (CK.eulerian1F k)

theorem CK.eulerian1_sf (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) : (eulerian1 k) (sf k f) = eulerian1F k f

@[simp]

theorem CK.eulerian1_one (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) 1 = 0

e⁽¹⁾ kills the unit: there are no positive-degree terms on the empty forest.

theorem CK.eulerian1_dot (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) (sf k [RTree.node []]) = sf k [RTree.node []]

e⁽¹⁾ fixes the generating primitive • (eigenvalue 1): only the j=1 term survives, with coefficient 1, and J(•) = •.

theorem CK.eulerian1_idem_dot (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) ((eulerian1 k) (sf k [RTree.node []])) = (eulerian1 k) (sf k [RTree.node []])

Idempotency on the primitive •: e⁽¹⁾(e⁽¹⁾ •) = e⁽¹⁾ •. Immediate from eulerian1_dot (since e⁽¹⁾ fixes •); likewise e⁽¹⁾ is idempotent on anything it fixes or kills.

NOTE (honest scope): the GENERAL projector identity e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ is false on this planar (Foissy) Hopf algebra — it is neither commutative nor cocommutative, and the Eulerian idempotents are orthogonal idempotents only in the (co)commutative case (Patras, Loday). Explicit counterexample (verified numerically in ConnesKreimerEval.lean): on the cherry, e⁽¹⁾∘e⁽¹⁾ and e⁽¹⁾ differ in the •·ℓ₂ vs ℓ₂·• terms — exactly the planar non-commutativity. Genuine idempotency (the Hodge/Eulerian decomposition) lives on the commutative quotient (A2 in the seam), not here.

e⁽¹⁾ fixes every primitive (Phase 1: the element-level primitive facts).

For primitive `x`: `ε(x)=0`, `J(x)=x`, and `J^{⋆k}(x)=0` for `k ≥ 2` (each higher factor must
absorb the unit, which `J` kills). These feed the operator identity in Phase 2. 

theorem CK.IsPrimitive.counit_zero (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) : (ε k) x = 0

A primitive element has zero counit (forced by the counit axiom (ε⊗id)∘Δ = 1⊗·).

theorem CK.Jc_ofConv_apply (k : Type u_1) [CommRing k] (x : H k) : (Jc k).ofConv x = x - (ε k) x • 1

J = id − u∘ε at the element level: J(x) = x − ε(x)·1.

theorem CK.Jc_ofConv_one (k : Type u_1) [CommRing k] : (Jc k).ofConv 1 = 0

J kills the unit.

theorem CK.Jc_pow_succ_ofConv_one (k : Type u_1) [CommRing k] (j : ℕ) : (Jc k ^ (j + 1)).ofConv 1 = 0

J^{⋆(j+1)} kills the unit (the first factor J(1)=0).

theorem CK.Jc_ofConv_primitive (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) : (Jc k).ofConv x = x

J fixes a primitive: J(x) = x.

theorem CK.Jc_pow_ofConv_primitive (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) (j : ℕ) : (Jc k ^ (j + 2)).ofConv x = 0

J^{⋆(k+2)} kills a primitive: each of the two top factors absorbs the unit (J(1)=0).

e⁽¹⁾ fixes every primitive (Phase 2: assembling the operator identity).

`e⁽¹⁾` agrees on degree-`≤N` elements with the finite truncation `Σ_{j≤N} c_j J^{⋆j}` (extra
terms vanish by nilpotency); on a primitive only the `j=1` term survives, giving `e⁽¹⁾(x)=x`. 

theorem CK.list_range_sum_eq {M : Type u_2} [AddCommMonoid M] (m : ℕ) (g : ℕ → M) : (List.map g (List.range m)).sum = ∑ j ∈ Finset.range m, g j

Bridge: a List.range map-sum equals the corresponding Finset.range sum.

noncomputable def CK.logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (N : ℕ) : H k →ₗ[k] H k

The degree-N truncation of log_⋆(id), as a linear map.

Equations

• CK.logTrunc k N = ∑ j ∈ Finset.range (N + 1), CK.eulerCoef k j • (CK.Jc k ^ j).ofConv

theorem CK.logTrunc_apply (k : Type u_1) [CommRing k] [Algebra ℚ k] (N : ℕ) (y : H k) : (logTrunc k N) y = ∑ j ∈ Finset.range (N + 1), eulerCoef k j • (Jc k ^ j).ofConv y

theorem CK.eulerian1F_eq_logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) (N : ℕ) (h : sizeF f ≤ N) : eulerian1F k f = (logTrunc k N) (sf k f)

On a basis forest of degree ≤ N, e⁽¹⁾ equals the degree-N truncation (nilpotency kills the surplus terms).

theorem CK.lmap_eq_sum (k : Type u_1) [CommRing k] (g : H k →ₗ[k] H k) (y : H k) : g y = Finsupp.sum y fun (a : FreeMonoid RTree) (b : k) => g (Finsupp.single a b)

A linear endomorphism of H is the basis-sum of its values on the singletons (proved by exact, sidestepping the MonoidAlgebra/Finsupp syntactic wall in rw).

theorem CK.eulerian1_eq_logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (x : H k) (N : ℕ) (hN : ∀ f ∈ x.support, sizeF f ≤ N) : (eulerian1 k) x = (logTrunc k N) x

e⁽¹⁾ agrees with the truncation logTrunc N on any element supported in degrees ≤ N.

theorem CK.eulerian1_primitive (k : Type u_1) [CommRing k] [Algebra ℚ k] {x : H k} (hx : IsPrimitive k x) : (eulerian1 k) x = x

e⁽¹⁾ fixes every primitive: e⁽¹⁾(x) = x for primitive x. Only the j=1 term of the log series survives (J(x)=x; j=0 has coefficient 0; j≥2 vanish), so e⁽¹⁾(x)=x. The primitives are exactly the eigenvalue-1 eigenspace of e⁽¹⁾.

A2 — the commutative quotient H_ab = H / ⟨ab − ba⟩

(Foissy's planar → commutative map).

Abelianizing the (forest) product turns the planar Hopf algebra into a commutative one. This is
the algebra step (S1): the quotient ring `RingQuot` by the commutator relation, shown
commutative.
The coproduct, counit and antipode descend in the following stones, giving the classical
(commutative) Connes–Kreimer / Butcher Hopf algebra, where the Eulerian idempotents become
genuine orthogonal idempotents. 

inductive CK.commRel (k : Type u_1) [CommRing k] : H k → H k → Prop

The commutator relation x·y ∼ y·x on H.

• mul {k : Type u_1} [CommRing k] (x y : H k) : commRel k (x * y) (y * x)

@[reducible, inline]

abbrev CK.Hab (k : Type u_1) [CommRing k] : Type u_1

The commutative quotient H_ab = H / ⟨ab − ba⟩.

Equations

• CK.Hab k = RingQuot (CK.commRel k)

noncomputable def CK.π (k : Type u_1) [CommRing k] : H k →ₐ[k] Hab k

The quotient algebra map π : H → H_ab.

Equations

• CK.π k = RingQuot.mkAlgHom k (CK.commRel k)

@[implicit_reducible]

noncomputable instance CK.instCommRingHab (k : Type u_1) [CommRing k] : CommRing (Hab k)

H_ab is commutative: the relation forces π(x)·π(y) = π(y)·x.

Equations

• CK.instCommRingHab k = { toRing := inferInstance, mul_comm := ⋯ }

theorem CK.π_surjective (k : Type u_1) [CommRing k] : Function.Surjective ⇑(π k)

theorem CK.π_mul_comm (k : Type u_1) [CommRing k] (x y : H k) : (π k) (x * y) = (π k) (y * x)

S2 — the coproduct descends to Delta_ab : H_ab → H_ab ⊗ H_ab.

noncomputable def CK.ΔAlg (k : Type u_1) [CommRing k] : H k →ₐ[k] TensorProduct k (H k) (H k)

Δ as an algebra homomorphism (the bialgebra coproduct), from Δ_one and Δ_mul.

Equations

• CK.ΔAlg k = AlgHom.ofLinearMap (CK.Δ k) ⋯ ⋯

theorem CK.ΔAlg_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : ((Algebra.TensorProduct.map (π k) (π k)).comp (ΔAlg k)) a = ((Algebra.TensorProduct.map (π k) (π k)).comp (ΔAlg k)) b

(π⊗π)∘Δ respects the commutator relation, since H_ab ⊗ H_ab is commutative.

noncomputable def CK.Δab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] TensorProduct k (Hab k) (Hab k)

The descended coproduct Delta_ab : H_ab → H_ab ⊗ H_ab.

Equations

• CK.Δab k = (RingQuot.liftAlgHom k) ⟨(Algebra.TensorProduct.map (CK.π k) (CK.π k)).comp (CK.ΔAlg k), ⋯⟩

theorem CK.Δab_π (k : Type u_1) [CommRing k] (x : H k) : (Δab k) ((π k) x) = (Algebra.TensorProduct.map (π k) (π k)) ((ΔAlg k) x)

The descent square commutes: Delta_ab ∘ π = (π⊗π) ∘ Δ.

S3 — the counit descends to epsilon_ab : H_ab → k.

theorem CK.εalg_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : (εalg k) a = (εalg k) b

ε respects the commutator relation (k is commutative).

noncomputable def CK.εab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] k

The descended counit epsilon_ab : H_ab → k.

Equations

• CK.εab k = (RingQuot.liftAlgHom k) ⟨CK.εalg k, ⋯⟩

theorem CK.εab_π (k : Type u_1) [CommRing k] (x : H k) : (εab k) ((π k) x) = (εalg k) x

S4 — H_ab is a coalgebra (coassoc + counit laws descend through π).

theorem CK.Hab_lhom_ext (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] {g₁ g₂ : Hab k →ₗ[k] M} (h : ∀ (x : H k), g₁ ((π k) x) = g₂ ((π k) x)) : g₁ = g₂

Extensionality on H_ab: a linear map out of H_ab is determined by its values on π.

theorem CK.εab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (εab k).toLinearMap ∘ₗ (Algebra.TensorProduct.map (π k) (π k)).toLinearMap = TensorProduct.map (ε k) (π k).toLinearMap

ε (right) counit naturality: (epsilon_ab⊗id)∘(π⊗π) = ε⊗π.

theorem CK.εab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (εab k).toLinearMap ∘ₗ (Algebra.TensorProduct.map (π k) (π k)).toLinearMap = TensorProduct.map (π k).toLinearMap (ε k)

ε (left) counit naturality: (id⊗epsilon_ab)∘(π⊗π) = π⊗ε.

theorem CK.rTensor_εab_comp_Δab (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (εab k).toLinearMap ∘ₗ (Δab k).toLinearMap = (TensorProduct.mk k k (Hab k)) 1

Left counitality on H_ab: (epsilon_ab ⊗ id) ∘ Delta_ab = 1 ⊗ ·.

theorem CK.lTensor_εab_comp_Δab (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (εab k).toLinearMap ∘ₗ (Δab k).toLinearMap = (TensorProduct.mk k (Hab k) k).flip 1

Right counitality on H_ab: (id ⊗ epsilon_ab) ∘ Delta_ab = · ⊗ 1.

theorem CK.Δab_π' (k : Type u_1) [CommRing k] (x : H k) : (Δab k) ((π k) x) = (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ((Δ k) x)

Delta_ab ∘ π = (π⊗π) ∘ Δ in purely linear (TensorProduct.map) form.

theorem CK.Δab_tl_π (k : Type u_1) [CommRing k] (x : H k) : (Δab k).toLinearMap ((π k) x) = (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ((Δ k) x)

Delta_ab ∘ π in .toLinearMap form (for use inside compositions).

theorem CK.Δab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (Δab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) (π k).toLinearMap ∘ₗ LinearMap.rTensor (H k) (Δ k)

Coproduct (right) naturality for the descent: (Delta_ab⊗id)∘(π⊗π) = ((π⊗π)⊗π)∘(Δ⊗id).

theorem CK.Δab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (Δab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ∘ₗ LinearMap.lTensor (H k) (Δ k)

Coproduct (left) naturality for the descent: (id⊗Delta_ab)∘(π⊗π) = (π⊗(π⊗π))∘(id⊗Δ).

theorem CK.coassoc_Hab (k : Type u_1) [CommRing k] : ↑(TensorProduct.assoc k (Hab k) (Hab k) (Hab k)) ∘ₗ LinearMap.rTensor (Hab k) (Δab k).toLinearMap ∘ₗ (Δab k).toLinearMap = LinearMap.lTensor (Hab k) (Δab k).toLinearMap ∘ₗ (Δab k).toLinearMap

Coassociativity on H_ab, descended from the planar coassociativity via π.

@[implicit_reducible]

noncomputable instance CK.instCoalgebraStructHab (k : Type u_1) [CommRing k] : CoalgebraStruct k (Hab k)

H_ab is a coalgebra (the commutative Connes–Kreimer coalgebra).

Equations

• CK.instCoalgebraStructHab k = { comul := (CK.Δab k).toLinearMap, counit := (CK.εab k).toLinearMap }

@[implicit_reducible]

noncomputable instance CK.instHabCoalg (k : Type u_1) [CommRing k] : Coalgebra k (Hab k)

Equations

• CK.instHabCoalg k = { toCoalgebraStruct := CK.instCoalgebraStructHab k, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

S5 — H_ab is a Bialgebra.

`Δab`, `εab` are algebra homs by construction, so the four `Bialgebra.mk'`
compatibilities are just `map_one`/`map_mul` (cf. planar `instCKBialg`, which
needed a separate `Δ_mul` because there `Δ` was not yet packaged as an AlgHom). 

@[implicit_reducible]

noncomputable instance CK.instHabBialg (k : Type u_1) [CommRing k] : Bialgebra k (Hab k)

Equations

• CK.instHabBialg k = Bialgebra.mk' k (CK.Hab k) ⋯ ⋯ ⋯ ⋯

S6 — the antipode descends to S_ab : H_ab → H_ab, giving HopfAlgebra k (H_ab).

S = antipode k is an algebra anti-homomorphism; composing with π into the COMMUTATIVE quotient H_ab turns it into a genuine algebra hom, so it lifts through RingQuot. The two antipode axioms then descend through π exactly like coassociativity in S4.

noncomputable def CK.SalgHom (k : Type u_1) [CommRing k] : H k →ₐ[k] Hab k

π ∘ S : H → H_ab as an algebra hom: on the commutative quotient the antipode anti-homomorphism becomes a homomorphism (π(S(ab)) = π(Sb·Sa) = π(Sa)·π(Sb)).

Equations

• CK.SalgHom k = AlgHom.ofLinearMap ((CK.π k).toLinearMap ∘ₗ CK.antipode k) ⋯ ⋯

theorem CK.SalgHom_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : (SalgHom k) a = (SalgHom k) b

π ∘ S respects the commutator relation (H_ab is commutative).

noncomputable def CK.Sab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] Hab k

The descended antipode S_ab : H_ab → H_ab.

Equations

• CK.Sab k = (RingQuot.liftAlgHom k) ⟨CK.SalgHom k, ⋯⟩

theorem CK.Sab_π (k : Type u_1) [CommRing k] (x : H k) : (Sab k) ((π k) x) = (π k) ((antipode k) x)

The descent square: S_ab ∘ π = π ∘ S.

theorem CK.mul'_π (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = (π k).toLinearMap ∘ₗ LinearMap.mul' k (H k)

mu_ab ∘ (π⊗π) = π ∘ μ (multiplication naturality, π an algebra hom).

theorem CK.Sab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (Sab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (π k).toLinearMap ∘ₗ LinearMap.rTensor (H k) (antipode k)

Antipode (left) naturality for the descent: (S_ab⊗id)∘(π⊗π) = (π⊗π)∘(S⊗id).

theorem CK.Sab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (Sab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (π k).toLinearMap ∘ₗ LinearMap.lTensor (H k) (antipode k)

Antipode (right) naturality for the descent: (id⊗S_ab)∘(π⊗π) = (π⊗π)∘(id⊗S).

theorem CK.lTensor_antipode_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

The (right-factor) left antipode identity, stated for antipode k rather than antipode' k (id ⋆ S = u∘ε re-expressed via antipode = antipode').

theorem CK.rTensor_Sab_Δab (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ LinearMap.rTensor (Hab k) (Sab k).toLinearMap ∘ₗ (Δab k).toLinearMap = Algebra.linearMap k (Hab k) ∘ₗ (εab k).toLinearMap

Left antipode identity on H_ab, descended through π.

theorem CK.lTensor_Sab_Δab (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ LinearMap.lTensor (Hab k) (Sab k).toLinearMap ∘ₗ (Δab k).toLinearMap = Algebra.linearMap k (Hab k) ∘ₗ (εab k).toLinearMap

Right antipode identity on H_ab, descended through π.

@[implicit_reducible]

noncomputable instance CK.instHopfAlgebraStructHab (k : Type u_1) [CommRing k] : HopfAlgebraStruct k (Hab k)

Equations

• CK.instHopfAlgebraStructHab k = { toBialgebra := CK.instHabBialg k, antipode := (CK.Sab k).toLinearMap }

@[implicit_reducible]

noncomputable instance CK.instHabHopf (k : Type u_1) [CommRing k] : HopfAlgebra k (Hab k)

H_ab is a Hopf algebra: the commutative Connes–Kreimer / Butcher Hopf algebra of rooted forests, obtained from the planar one by the abelianization quotient.

Equations

• CK.instHabHopf k = { toHopfAlgebraStruct := CK.instHopfAlgebraStructHab k, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

Toward the Eulerian-idempotent payoff — Adams operators on H_ab.

On the COMMUTATIVE H_ab the Eulerian idempotents e⁽ⁱ⁾ become orthogonal idempotents (Patras/Loday), so e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ HOLDS (unlike the planar non-idempotency of D1). The principled route is via the Adams operators Ψⁿ: on a commutative Hopf algebra each Ψⁿ is an algebra morphism, whence Ψᵖ∘Ψq = Ψ^{pq}, whence the e⁽ⁱ⁾ are the orthogonal eigen-projectors.

Brick 1 (no commutativity yet): the Adams operators on H_ab, and their naturality through π (Ψⁿ_ab ∘ π = π ∘ Ψⁿ), which both defines Ψⁿ_ab and ties it to the planar Ψⁿ.

noncomputable def CK.adamsAb (k : Type u_1) [CommRing k] (n : ℕ) : Hab k →ₗ[k] Hab k

The Adams operators Ψⁿ = id^{⋆n} on H_ab (convolution powers of the identity).

Equations

• CK.adamsAb k n = (WithConv.toConv LinearMap.id ^ n).ofConv

theorem CK.conv_apply_ab (k : Type u_1) [CommRing k] (F G : Hab k →ₗ[k] Hab k) (x : Hab k) : (WithConv.toConv F * WithConv.toConv G).ofConv x = (LinearMap.mul' k (Hab k)) ((TensorProduct.map F G) ((Δab k).toLinearMap x))

Element-level convolution on H_ab: (F⋆G)(x) = mu_ab((F⊗G)(Delta_ab x)).

theorem CK.adamsAb_succ_apply (k : Type u_1) [CommRing k] (n : ℕ) (x : Hab k) : (adamsAb k (n + 1)) x = (LinearMap.mul' k (Hab k)) ((TensorProduct.map LinearMap.id (adamsAb k n)) ((Δab k).toLinearMap x))

Ψⁿ⁺¹_ab = id ⋆ Ψⁿ_ab evaluated.

theorem CK.adamsAb_natural (k : Type u_1) [CommRing k] (n : ℕ) : adamsAb k n ∘ₗ (π k).toLinearMap = (π k).toLinearMap ∘ₗ adams k n

Adams naturality: Ψⁿ_ab ∘ π = π ∘ Ψⁿ. The planar Adams operators descend to H_ab through the bialgebra quotient map π.

Brick 2 (commutativity enters): each Adams operator Ψⁿ is an ALGEBRA morphism on the commutative H_ab. We package Ψⁿ as an AlgHom built by composition: Ψⁿ⁺¹ = mu_ab∘(id⊗Ψⁿ)∘Delta_ab. This is a composite of the algebra homs Delta_ab, id⊗Ψⁿ, and mu_ab, and the multiplication is an algebra hom precisely because H_ab is commutative.

noncomputable def CK.adamsAbHom (k : Type u_1) [CommRing k] : ℕ → Hab k →ₐ[k] Hab k

Ψⁿ packaged as an algebra hom on the commutative H_ab (Ψ₀ = u∘ε, Ψⁿ⁺¹ = mu_ab ∘ (id ⊗ Ψⁿ) ∘ Delta_ab).

Equations

• CK.adamsAbHom k 0 = (Algebra.ofId k (CK.Hab k)).comp (CK.εab k)
• CK.adamsAbHom k n.succ = (Algebra.TensorProduct.lmul' k).comp ((Algebra.TensorProduct.map (AlgHom.id k (CK.Hab k)) (CK.adamsAbHom k n)).comp (CK.Δab k))

theorem CK.adamsAbHom_toLinearMap (k : Type u_1) [CommRing k] (n : ℕ) : (adamsAbHom k n).toLinearMap = adamsAb k n

The algebra-hom Ψⁿ and the convolution-power Ψⁿ agree as linear maps.

theorem CK.adamsAb_mul (k : Type u_1) [CommRing k] (n : ℕ) (a b : Hab k) : (adamsAb k n) (a * b) = (adamsAb k n) a * (adamsAb k n) b

Brick 2 — Ψⁿ is an algebra morphism on H_ab: Ψⁿ(ab) = Ψⁿ(a)·Ψⁿ(b). The key commutative-Hopf fact behind the orthogonality of the Eulerian idempotents.

Brick 3: the Adams composition law Ψᵖ ∘ Ψq = Ψ^{pq}. Post-composition by an algebra hom distributes over convolution (LinearMap.algHom_comp_convMul_distrib), so an algebra-hom φ post-composed with Ψᵖ = id^{⋆p} gives (φ ∘ id)^{⋆p} = (toConv φ)^p. Taking φ = Ψq gives Ψq ∘ Ψᵖ = (Ψq)^{⋆p} = id^{⋆qp} = Ψ^{qp}.

theorem CK.algHom_comp_adamsAb (k : Type u_1) [CommRing k] (φ : Hab k →ₐ[k] Hab k) (p : ℕ) : φ.toLinearMap ∘ₗ adamsAb k p = (WithConv.toConv φ.toLinearMap ^ p).ofConv

An algebra hom φ post-composed with the Adams operator Ψᵖ is the p-th convolution power of φ itself: φ ∘ Ψᵖ = (toConv φ)^p in WithConv.

theorem CK.adamsAb_comp (k : Type u_1) [CommRing k] (p q : ℕ) : adamsAb k p ∘ₗ adamsAb k q = adamsAb k (p * q)

Brick 3 — the Adams composition law Ψᵖ ∘ Ψq = Ψ^{pq} on the commutative H_ab. The Adams (Hopf-power) operators form a commuting family of algebra endomorphisms realising the multiplicative monoid (ℕ, ·); this is the structural reason the Eulerian idempotents are orthogonal.

Brick 4 — toward e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ on the commutative H_ab, via the finite-difference engine.

The route AVOIDS the full Eulerian decomposition / Vandermonde inversion. The point:
if `v` is an Adams eigenvector with `Ψⁱ(v) = i·v` for all `i`, then expanding
`J^{⋆j} = (id − u∘ε)^{⋆j}` into Adams operators and applying to `v` collapses
each `J^{⋆j}(v)` to a scalar multiple of `v` by the finite-difference identity below.
Hence `e⁽¹⁾` is the identity on its own image. 

theorem CK.alternating_choose_weighted (j : ℕ) : ∑ i ∈ Finset.range (j + 1), (-1) ^ (j - i) * ↑(j.choose i) * ↑i = if j = 1 then 1 else 0

Finite-difference engine: the j-th finite difference of the identity sequence i ↦ i, ∑ᵢ (-1)^{j-i} C(j,i)·i = δ_{j,1}. This collapses the convolution-log of an Adams eigenvector to its weight-1 component, which is the combinatorial heart of the Eulerian idempotency on H_ab.

Brick B (binomial expansion) — J_ab^{⋆j} into Adams operators on the commutative H_ab. Toward e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾: expand the convolution-log's J^{⋆j} into the Adams basis so that, on an Adams eigenvector, alternating_choose_weighted collapses it.

theorem CK.JcAb_pow_ofConv_eq_adams_sum (k : Type u_1) [CommRing k] (j : ℕ) (x : Hab k) : ((WithConv.toConv LinearMap.id - 1) ^ j).ofConv x = ∑ i ∈ Finset.range (j + 1), ((-1) ^ (j - i) * ↑(j.choose i)) • (adamsAb k i) x

Brick A scaffolding — J^{⋆j} naturality through π and per-degree nilpotency on H_ab.

theorem CK.Jc_pow_ofConv_eq_adams_sum (k : Type u_1) [CommRing k] (j : ℕ) (z : H k) : (Jc k ^ j).ofConv z = ∑ i ∈ Finset.range (j + 1), ((-1) ^ (j - i) * ↑(j.choose i)) • (adams k i) z

theorem CK.Jc_pow_ofConv_natural (k : Type u_1) [CommRing k] (j : ℕ) (z : H k) : (π k) ((Jc k ^ j).ofConv z) = ((WithConv.toConv LinearMap.id - 1) ^ j).ofConv ((π k) z)

theorem CK.JcAb_pow_ofConv_sf_eq_zero (k : Type u_1) [CommRing k] (n : ℕ) (f : Forest) (h : sizeF f < n) : ((WithConv.toConv LinearMap.id - 1) ^ n).ofConv ((π k) (sf k f)) = 0

Brick A core — the Φ_p ring-hom step: post-composition by Ψᵖ (adamsAb p, an algebra hom) is a ⋆-ring hom, sending J_ab ↦ Yᵖ − 1 (Y = toConv id_ab). This is Ψᵖ ∘ e = log(Yᵖ).

theorem CK.algHom_comp_convPow (k : Type u_1) [CommRing k] (φ : Hab k →ₐ[k] Hab k) (g : WithConv (Hab k →ₗ[k] Hab k)) (j : ℕ) : φ.toLinearMap ∘ₗ (g ^ j).ofConv = (WithConv.toConv (φ.toLinearMap ∘ₗ g.ofConv) ^ j).ofConv

theorem CK.adamsAb_comp_JcAb_pow (k : Type u_1) [CommRing k] (p j : ℕ) (y : Hab k) : (adamsAb k p) (((WithConv.toConv LinearMap.id - 1) ^ j).ofConv y) = ((WithConv.toConv LinearMap.id ^ p - 1) ^ j).ofConv y

Brick A step 2 — eval₂ plumbing: bridge the PowerSeries coeff identity (coeff_logTrunc_pow) to the convolution sums via eval₂ (X ↦ J_ab), then kill high powers with nilpotency.

noncomputable def CK.JcAb (k : Type u_1) [CommRing k] : WithConv (Hab k →ₗ[k] Hab k)

J_ab = id − u∘ε on H_ab, as a convolution-ring element.

Equations

• CK.JcAb k = WithConv.toConv LinearMap.id - 1

noncomputable def CK.smulOne (k : Type u_1) [CommRing k] : k →+* WithConv (Hab k →ₗ[k] Hab k)

r ↦ r • 1 as a ring hom k →+* WithConv(H_ab) (image central; convCommRing).

Equations

• CK.smulOne k = { toFun := fun (r : k) => r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem CK.eulerCoef_eq_coeff_log (k : Type u_1) [CommRing k] [Algebra ℚ k] (j : ℕ) : eulerCoef k j = (PowerSeries.coeff j) (PowerSeries.log k)

The Eulerian coefficient (-1)^{j+1}/j equals the j-th coefficient of the formal log.

theorem CK.eval₂_ofConv (k : Type u_1) [CommRing k] (P : Polynomial k) (w : Hab k) : (Polynomial.eval₂ (smulOne k) (JcAb k) P).ofConv w = ∑ m ∈ Finset.range (P.natDegree + 1), P.coeff m • (JcAb k ^ m).ofConv w

eval₂ smulOne J_ab P, applied through .ofConv to w, is the explicit sum Σₘ (P.coeff m) • (J_ab^m).ofConv w.

theorem CK.PR_coeff (k : Type u_1) [CommRing k] [Algebra ℚ k] (N m : ℕ) (hm : m ≤ N) : (∑ j ∈ Finset.range (N + 1), Polynomial.C ((PowerSeries.coeff j) (PowerSeries.log k)) * Polynomial.X ^ j).coeff m = (PowerSeries.coeff m) (PowerSeries.log k)

The truncated ∑ⱼ cⱼ X^j polynomial has coeff m = cₘ for m ≤ N.

theorem CK.star_identity (k : Type u_1) [CommRing k] [Algebra ℚ k] (p N : ℕ) (w : Hab k) (hnil : ∀ (m : ℕ), N < m → (JcAb k ^ m).ofConv w = 0) : ∑ j ∈ Finset.range (N + 1), (PowerSeries.coeff j) (PowerSeries.log k) • ((WithConv.toConv LinearMap.id ^ p - 1) ^ j).ofConv w = ↑p • ∑ j ∈ Finset.range (N + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv w

(★) — the eigen-transport identity on a per-degree-nilpotent w: applying Ψᵖ to the truncated convolution-log scales it by p. Proven by evaluating the polynomial coeff_logTrunc_pow identity at J_ab (eval₂), killing the surplus J_ab^{>N} by nilpotency.

theorem CK.pi_eulerian1_eq (k : Type u_1) [CommRing k] [Algebra ℚ k] (y : H k) (M : ℕ) (hMy : ∀ a ∈ y.support, sizeF a ≤ M) : (π k) ((eulerian1 k) y) = ∑ j ∈ Finset.range (M + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv ((π k) y)

π(e⁽¹⁾ y) as a truncated convolution-log sum on H_ab, for any degree bound M ≥ deg(y).

theorem CK.adamsAb_eigen_basis (k : Type u_1) [CommRing k] [Algebra ℚ k] (p : ℕ) (f : Forest) : (adamsAb k p) ((π k) ((eulerian1 k) (sf k f))) = ↑p • (π k) ((eulerian1 k) (sf k f))

Adams eigen-relation on a basis forest: Ψᵖ(π(e⁽¹⁾(sf f))) = p · π(e⁽¹⁾(sf f)).

theorem CK.adamsAb_eigen (k : Type u_1) [CommRing k] [Algebra ℚ k] (p : ℕ) (x : H k) : (adamsAb k p) ((π k) ((eulerian1 k) x)) = ↑p • (π k) ((eulerian1 k) x)

Adams eigen-relation (general): Ψᵖ(π(e⁽¹⁾ x)) = p · π(e⁽¹⁾ x) for all x.

Brick C — the finite-difference collapse: on an Adams eigenvector the convolution-log truncation collapses to the eigenvector itself (only the weight-1 term survives).

theorem CK.brickC (k : Type u_1) [CommRing k] [Algebra ℚ k] (v : Hab k) (M : ℕ) (hM : 1 ≤ M) (heig : ∀ (i : ℕ), (adamsAb k i) v = ↑i • v) : ∑ j ∈ Finset.range (M + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv v = v

Brick C (collapse). On an Adams eigenvector v (Ψⁱ(v) = i·v), the truncated convolution-log is the identity: Σⱼ≤M cⱼ · J_ab^{⋆j}(v) = v (M ≥ 1). The J_ab^{⋆j} expands into Adams ops, the eigen-relation turns each into a scalar, and alternating_choose_weighted kills all but j = 1.

theorem CK.eulerian1_idem_ab (k : Type u_1) [CommRing k] [Algebra ℚ k] (x : H k) : (π k) ((eulerian1 k) ((eulerian1 k) x)) = (π k) ((eulerian1 k) x)

e⁽¹⁾ ∘ e⁽¹⁾ = e⁽¹⁾ on the commutative H_ab (the Eulerian idempotency, via π). The first Eulerian idempotent is genuinely idempotent on the abelianized Connes–Kreimer / Butcher Hopf algebra. Combines pi_eulerian1_eq, the Adams eigen-relation adamsAb_eigen, and the Brick-C collapse.