The EES(2,5;x) family

The three-stage EES(2,5;x) Runge–Kutta family (arXiv:2507.21006, Proposition 8.4; arXiv:2509.20599, Proposition 2.1), defined for x ∉ {1, ±1/2}:

c = (0, (1+2x)/(4(1-x)), 3/(4(1-x))), b = (x, 1/2, 1/2 - x).

We prove, for every admissible parameter x over any field of characteristic ≠ 2:

• the family is explicit, and specialises to the concrete ees25 scheme at x = 1/4;
• the family is Williamson 2N (arXiv:2509.20599, Proposition 3.1), with the closed-form two-register coefficients of equations (14)–(15);
• the stability coefficients Σᵢ bᵢ = 1, Σᵢ bᵢ cᵢ = 1/2 and Σᵢⱼ bᵢ aᵢⱼ cⱼ = 1/8 are independent of x, so the linear stability polynomial of the whole family is R(ρ) = 1 + ρ + ρ²/2 + ρ³/8 (the algebraic core of arXiv:2509.20599, Theorem 2.2).

def BSeries.RungeKutta.ees25 {R : Type v} [Field R] (x : R) : RungeKutta (Fin 3) R

The three-stage EES(2,5;x) family (arXiv:2507.21006, Proposition 8.4), defined for x ∉ {1, ±1/2}.

Equations

• One or more equations did not get rendered due to their size.

theorem BSeries.RungeKutta.isExplicit_ees25 {R : Type v} [Field R] (x : R) : (ees25 x).IsExplicit

The family is explicit for every parameter.

def BSeries.RungeKutta.ees25LowStorage {R : Type v} [Field R] (x : R) : LowStorage 3 R

The Williamson 2N coefficients of the EES(2,5;x) family (arXiv:2509.20599, equations (14)–(15)).

Equations

• One or more equations did not get rendered due to their size.

Entrywise evaluation of the family tableau and its low-storage data; each is a definitional reduction of a vector literal.

theorem BSeries.RungeKutta.toRK_ees25LowStorage {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) : (ees25LowStorage x).toRK = ees25 x

The closed-form two-register coefficients (14)–(15) induce exactly the EES(2,5;x) Butcher tableau.

theorem BSeries.RungeKutta.isWilliamson2N_ees25 {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) : (ees25 x).IsWilliamson2N

The entire EES(2,5;x) family is Williamson 2N (arXiv:2509.20599, Proposition 3.1), realised by the closed-form two-register coefficients (14)–(15).

The CF-EES(2,5;x) family

Bazavov's commutator-free lift of the low-storage coefficients produces the CF-EES(2,5;x) integrator on any space carrying an exponential action (arXiv:2509.20599, equation (16)).

noncomputable def BSeries.RungeKutta.cfEES25 {R : Type v} [Field R] (x : R) : CommutatorFreeMethod (Fin 3) R

The CF-EES(2,5;x) commutator-free method (arXiv:2509.20599, equation (16)): the Bazavov lift of the Williamson 2N form of EES(2,5;x).

Equations

• BSeries.RungeKutta.cfEES25 x = (BSeries.RungeKutta.ees25LowStorage x).toCommutatorFree

theorem BSeries.RungeKutta.cfEES25_step_translation {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) {E : Type w} [AddCommMonoid E] [Module R E] (K : Fin 3 → E) (y : E) : (cfEES25 x).step (ExponentialAction.translation E) K y = y + ∑ j : Fin 3, (ees25 x).b j • K j

On a flat space CF-EES(2,5;x) collapses to the classical EES(2,5;x) step (arXiv:2509.20599, Section 3): under the translation action the commutator-free step is the Runge–Kutta update y + Σⱼ bⱼ Kⱼ.

theorem BSeries.RungeKutta.cfEES25_stagePoint_translation {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) {E : Type w} [AddCommMonoid E] [Module R E] (K : Fin 3 → E) (i : Fin 3) (y : E) : (cfEES25 x).stagePoint (ExponentialAction.translation E) K i y = y + ∑ j : Fin 3, (ees25 x).A i j • K j

The stage points of CF-EES(2,5;x) on a flat space are the classical Runge–Kutta stage values.

The paper's reference point x = 1/10

arXiv:2509.20599 fixes x = 1/10 (minimising the leading error) and records the resulting numerical tables; we machine-check them against the general closed forms.

theorem BSeries.RungeKutta.ees25LowStorage_tenth : (ees25LowStorage (1 / 10)).B = ![1 / 3, 15 / 16, 2 / 5] ∧ (ees25LowStorage (1 / 10)).A = ![0, -7 / 15, -35 / 32]

At x = 1/10 the Williamson coefficients evaluate to B = (1/3, 15/16, 2/5), A = (0, -7/15, -35/32) (arXiv:2509.20599, Appendix D).

theorem BSeries.RungeKutta.beta_ees25LowStorage_tenth (l i : Fin 3) : (ees25LowStorage (1 / 10)).beta l i = ![![1 / 3, 0, 0], ![-7 / 16, 15 / 16, 0], ![49 / 240, -7 / 16, 2 / 5]] l i

The exponential weight table of CF-EES(2,5;1/10) (arXiv:2509.20599, Proposition D.1): row l lists the coefficients β_{l,i} of the slopes inside the l-th exponential.

theorem BSeries.RungeKutta.sum_beta_eq_b_ees25LowStorage_tenth (i : Fin 3) : ∑ l : Fin 3, (ees25LowStorage (1 / 10)).beta l i = (ees25 (1 / 10)).b i

The Euclidean consistency check of Proposition D.1: the columns of the exponential weight table sum to the quadrature weights, Σ_l β_{l,i} = b_i.

Stability coefficients

The linear stability polynomial of an explicit three-stage scheme is R(ρ) = 1 + (Σᵢ bᵢ) ρ + (Σᵢ bᵢ cᵢ) ρ² + (Σᵢⱼ bᵢ aᵢⱼ cⱼ) ρ³. The three coefficients below are independent of x, giving R(ρ) = 1 + ρ + ρ²/2 + ρ³/8 for the whole family — the algebraic core of arXiv:2509.20599, Theorem 2.2.

theorem BSeries.RungeKutta.weightBullet_ees25 {R : Type v} [Field R] {x : R} (h2 : 2 ≠ 0) : (ees25 x).weightBullet = 1

The quadrature weights of EES(2,5;x) sum to one, for every x (the ρ-coefficient of the stability polynomial).

theorem BSeries.RungeKutta.weight_chain2_ees25 {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) : (ees25 x).weight HopfAlgebras.PTree.chain2 = 1 / 2

The ρ²-coefficient of the stability polynomial of EES(2,5;x) is 1/2, independent of x (equivalently, the order-two chain condition holds for the whole family).

theorem BSeries.RungeKutta.weight_chain3_ees25 {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) : (ees25 x).weight HopfAlgebras.PTree.chain3 = 1 / 8

The ρ³-coefficient of the stability polynomial of EES(2,5;x) is 1/8, independent of x (arXiv:2509.20599, Theorem 2.2).

Order two, symbolically

theorem BSeries.RungeKutta.hasOrder_two_ees25 {R : Type v} [Field R] {x : R} (hx1 : x ≠ 1) (hx2 : 2 * x ≠ 1) (hx3 : 2 * x ≠ -1) (h2 : 2 ≠ 0) : (ees25 x).HasOrder 2

EES(2,5;x) has order two for every admissible parameter over any field of characteristic ≠ 2.

The generic parameter: EES(2,5;X) is an EES(2,5) scheme

Instantiating at the generic parameter X : CRatFunc ℚ — i.e. working with rational functions of an indeterminate — the remaining order conditions of arXiv:2507.21006, Section 8 hold as identities of rational functions, verified by native_decide over the computable field CRatFunc ℚ.

theorem BSeries.RungeKutta.hasOrder_two_ees25_generic : (ees25 CRatFunc.X).HasOrder 2

EES(2,5;X) has order two at the generic parameter.

theorem BSeries.RungeKutta.not_hasOrder_three_ees25_generic : ¬(ees25 CRatFunc.X).HasOrder 3

EES(2,5;X) does not have order three: the cherry-tree condition fails as an identity of rational functions.

theorem BSeries.RungeKutta.hasAntisymOrder_five_ees25_generic : ForestAlgebra.Character.HasAntisymOrder (ees25 CRatFunc.X).series.toCharacter 5

EES(2,5;X) has antisymmetric order five at the generic parameter: the composed-weight identities hold as identities of rational functions on all planar trees of order at most five.

theorem BSeries.RungeKutta.not_hasAntisymOrder_six_ees25_generic : ¬ForestAlgebra.Character.HasAntisymOrder (ees25 CRatFunc.X).series.toCharacter 6

EES(2,5;X) does not have antisymmetric order six: the six-chain is a witness at the generic parameter.

theorem BSeries.RungeKutta.isEES_ees25_generic : (ees25 CRatFunc.X).IsEES 2 5

The EES(2,5;x) family is an EES(2,5) scheme at the generic parameter (arXiv:2507.21006, Section 8): explicit, of order exactly two, and of antisymmetric order exactly five, as identities of rational functions in the parameter.