How a Tree Forgets Its Order: the Eulerian idempotent and the Adams spectrum on the commutative Connes–Kreimer–Butcher Hopf algebra of rooted trees, machine-checked in Lean 4

A companion to How a Tree Remembers Its Cuts (Zenodo 10.5281/zenodo.20762280), which built the planar (Foissy, noncommutative) Connes–Kreimer / Butcher Hopf algebra of rooted trees in Lean 4 / Mathlib and left the commutative quotient and the spectral theory of its operators open. This development closes both, sorry-free. First, the commutative algebra Hab = H/(ab−ba) — the classical Butcher / Connes–Kreimer algebra — is built as a Mathlib HopfAlgebra instance (CK.instHabHopf) by descending the planar coproduct, counit and antipode through Mathlib's RingQuot. Second, the Adams ladder Ψn = id⋆n is run to its spectral payoff: the first Eulerian idempotent e(1) = log⋆(id) is proved idempotent, e(1)∘e(1) = e(1) (CK.eulerian1_idem_ab) — exactly the property that fails on the planar algebra (the cherry counterexample, also formalized), so commutativity is the operative hypothesis, not an incidental convenience. The proof avoids the textbook Vandermonde inversion, routing through a small piece of formal logarithm calculus on power series (log(fg)=log f+log g, log(fn)=n·log f), proved by uniqueness of formal antiderivatives with no analysis (PowerSeries.logOf_mul, logOf_pow — currently absent from Mathlib, a candidate for upstream inclusion), transported into the convolution algebra by the eigen-relation Ψi∘e(1) = i·e(1) and a finite-difference collapse. All headline results are sorry-free; #print axioms reports only [propext, Classical.choice, Quot.sound]. The mathematics is classical throughout (Adams; Solomon; Loday–Reutenauer–Patras; Aguiar–Lauve; Butcher; Connes–Kreimer; Foissy); the contribution is the certified instance and the formalized planar counterexample. Toolchain Lean v4.30.0-rc2, Mathlib rev 701fb6e9c3. The deposit includes the English and Spanish editions of the paper and the full Lean source.