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. Kimi K3 by Moonshot AI was used in the LLM-guided discovery and preparation pipeline, including development and refinement of the prefix-state invariant and assistance with formalization and manuscript preparation. Kimi K3 is an AI system and is not an author. This is a machine-verified preprint and has not been independently peer reviewed.
Complete verification artifact:https://doi.org/10.5281/zenodo.21764742
Public source repository:https://github.com/arex1337/williamson-order-three