How a Tree Remembers Its Cuts: the Connes--Kreimer--Foissy Hopf Algebra of Rooted Trees, Machine-Checked in Lean 4

A machine-checked formalization in Lean 4 / Mathlib of the Connes--Kreimer / Butcher / Foissy Hopf algebra of (planar) rooted trees — the combinatorial Hopf algebra behind perturbative renormalization and the order theory of Runge--Kutta methods. The admissible-cut coproduct, its coassociativity (proved up to List.Perm and lifted to an equality of Mathlib linear maps), the bialgebra compatibility, and a connected-graded antipode are assembled into a genuine Mathlib HopfAlgebra instance, all sorry-free; #print axioms reports only propext, Classical.choice, Quot.sound. To the best of our knowledge — after a documented search of Lean/Mathlib, the Isabelle/HOL Archive of Formal Proofs, and Coq/Rocq — this is the first combinatorial renormalization Hopf algebra of rooted trees registered in any proof assistant. The mathematics is classical throughout; the contribution is the formalization and a reusable certified core. This is the planar (Foissy, noncommutative) version; the commutative quotient, B-series order conditions, the free pre-Lie algebra, and Birkhoff/BPHZ renormalization are deferred follow-on work. A large language model was used as a coding assistant; every statement was independently checked by the Lean kernel, and all mathematics and claims are the author's. English and Spanish editions of the paper are included, with the Lean source.