Williamson 2N-storage Runge-Kutta methods can be lifted to Lie groups by replacing each additive low-storage update with an exponential update. The complete three-stage, third-order family was known to retain order three, while the same-order claim for methods with more stages remained conjectural. This preprint proves the order-three claim for every finite stage count.
For Owren's ordered tensor t2 and the classical moments M0 = b^T 1, M1 = b^T c, M2 = b^T c^2, and MAc = b^T Ac, every Williamson A-form coefficient sequence satisfies the division-free identity 2 t2(c,1) = M0 M1 - M2 + MAc. Together with the polarization identity t2(1,c) + t2(c,1) = M0 M1, the four classical third-order Runge-Kutta conditions imply Owren's one additional third-order commutator-free condition.
The finite coefficient theorem is machine-checked in Lean 4 and Mathlib with zero sorry, admit, or custom axioms. Exact symbolic code independently checks the recurrence, published rational examples, a non-Williamson negative control, and the noncommutative product convention. The Lean development does not formalize the ordered-tree completeness or analytic convergence theorem; the Lie-group order-three corollary invokes Owren's published theory.
T. Alexander Lystad is the human author and is responsible for the release. OpenAI GPT-5.6 Sol was used throughout the recorded LLM-guided discovery and preparation pipeline, including development and refinement of the prefix-state invariant, exact-checker development, formalization, auditing, and manuscript preparation. GPT-5.6 Sol is an AI system and is not an author. Version 1.0.1 corrects the model attribution in version 1.0.0; the mathematical result and verification certificates are unchanged. This is a machine-verified preprint and has not been independently peer reviewed.