An explicit 13-stage Runge-Kutta method of order 9 with exact algebraic coefficients

We give an explicit 13-stage Runge-Kutta method of order 9 whose coefficients are real algebraic numbers in a totally real number field of degree 16, and we verify all 486 order conditions in exact rational arithmetic. This proves that the minimal number of stages a(9) of an explicit Runge-Kutta method of order 9 satisfies a(9) <= 13. Together with Butcher's lower bound s >= p + 3 for order p >= 8, this gives 12 <= a(9) <= 13 (OEIS A187102). The method is not the 13-stage method that Khashin found numerically in 2009. It lies on a second five-dimensional component of the solution set, on which four weights and eight coupling coefficients vanish, three nodes coincide, and the weights form the interpolatory quadrature rule of nine nodes. Four programs, from three separate sources, confirm the exact check; one of them uses only the integer arithmetic of a stock Python interpreter and runs in about a minute. The search that produced the method, which ends in a 25000-digit refinement and a lattice reconstruction, is described but is not part of the proof. The ancillary zip holds the exact data and the checking scripts. To recheck the proof with no packages, unzip it and run, from the anc folder: python3 scripts/purepy_exact_check.py results/sigma_rur_inner1_tower.json