What Order a Method Knows: certified Runge–Kutta order conditions over rooted trees, machine-checked in Lean 4

Machine-checked Butcher order conditions for Runge–Kutta methods in Lean 4, sorry-free and depending only on the three standard axioms of classical Mathlib (propext, Classical.choice, Quot.sound). A small computable engine (order, density gamma, the Butcher elementary weight Phi) plus a keystone reducing the infinite family of order conditions to a finite, decidable catalogue check, discharged for Euler (order 1), the explicit trapezoid (order 2), classical RK4 (order 4), Dormand–Prince DOPRI5 (order 5, the default in MATLAB ode45 / SciPy RK45), and the 3-stage Gauss–Legendre method, fully implicit with coefficients in Q(sqrt 15), certified to full order 6 via an integer Z[sqrt 15] reformulation closed by 'decide'. Negative certificates pin the order exactly. This is the applied payoff of the rooted-tree Hopf-algebra series: the elementary weight is a character of the Connes–Kreimer/Butcher Hopf algebra, and a method has order p iff that character agrees with the exact flow on trees of order at most p. The attached archive contains the self-contained Lean source (ButcherOrder.lean) and the independent Python/Sage cross-checks. A large language model was used as a coding assistant; every statement was independently checked by the Lean kernel, and all mathematical decisions and claims are the author's.