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.
Attribution correction, 3 August 2026: This version 1.0.0 record and its immutable PDF originally misidentified Kimi K3 as the AI system used. The recorded model was OpenAI GPT-5.6 Sol, 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. T. Alexander Lystad is the human author and is responsible for the release. The mathematical result and verification certificates are unchanged. The corrected version 1.0.1 is available at https://doi.org/10.5281/zenodo.21770872. This is a machine-verified preprint and has not been independently peer reviewed.