Williamson 2N-storage Runge–Kutta schemes

A Williamson low-storage scheme advances an s-stage Runge–Kutta step using only two registers via the recurrence

δ_l = A_l δ_{l-1} + h K_l, Y_l = Y_{l-1} + B_l δ_l.

Unrolling the recurrence expresses each register update as a linear combination of the stage slopes with weights β_{l,j} = B_l A_l A_{l-1} ⋯ A_{j+1}, which induces a Butcher tableau. Bazavov's criterion (arXiv:2509.20599, Theorem 3.1) characterises the explicit tableaux arising this way:

a_{ik} (b_j - a_{kj}) = (a_{ij} - a_{kj}) b_k whenever k = j + 1 ≤ i.

We prove both directions, formalise Bazavov's commutator-free lift of a low-storage scheme (arXiv:2509.20599, equation (4)) together with its collapse to the classical Runge–Kutta step under a flat (translation) exponential action — the structural input for the CF-EES lifts of the EES(2,5;x) and EES(2,7;x) families (arXiv:2509.20599, Proposition 3.1).

References

• Williamson, Low-storage Runge-Kutta schemes
• Bazavov, Low-storage Runge-Kutta schemes and commutator-free Lie group methods
• Shmelev, Thompson, Salvi, arXiv:2509.20599, Section 3 and Appendix D

theorem BSeries.RungeKutta.ext {ι : Type u_1} {R : Type v} {rk₁ rk₂ : RungeKutta ι R} (hA : ∀ (i j : ι), rk₁.A i j = rk₂.A i j) (hb : ∀ (j : ι), rk₁.b j = rk₂.b j) : rk₁ = rk₂

Tableaux agreeing entrywise are equal.

structure BSeries.RungeKutta.LowStorage (s : ℕ) (R : Type v) : Type v

Low-storage (Williamson 2N) coefficient data for an s-stage scheme: the two-register recurrence δ_l = A_l δ_{l-1} + h K_l, Y_l = Y_{l-1} + B_l δ_l. The leading coefficient A 0 is never used.

• A : Fin s → R
• B : Fin s → R

def BSeries.RungeKutta.LowStorage.prodA {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (j l : ℕ) : R

The product A_{j+1} A_{j+2} ⋯ A_l of recurrence coefficients, over natural indices (empty product when l ≤ j).

Equations

• ls.prodA j l = ∏ k ∈ Finset.Ico (j + 1) (l + 1), if h : k < s then ls.A ⟨k, h⟩ else 1

@[simp]

theorem BSeries.RungeKutta.LowStorage.prodA_self {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (j : ℕ) : ls.prodA j j = 1

theorem BSeries.RungeKutta.LowStorage.prodA_succ_bot {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {j l : ℕ} (h : j < l) (hs : j + 1 < s) : ls.prodA j l = ls.A ⟨j + 1, hs⟩ * ls.prodA (j + 1) l

def BSeries.RungeKutta.LowStorage.beta {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (l j : Fin s) : R

The unrolled slope weights: β_{l,j} = B_l A_l ⋯ A_{j+1} for j ≤ l, and 0 otherwise.

Equations

• ls.beta l j = if j ≤ l then ls.B l * ls.prodA ↑j ↑l else 0

@[simp]

theorem BSeries.RungeKutta.LowStorage.beta_self {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (j : Fin s) : ls.beta j j = ls.B j

theorem BSeries.RungeKutta.LowStorage.beta_eq_zero_of_lt {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {l j : Fin s} (h : l < j) : ls.beta l j = 0

theorem BSeries.RungeKutta.LowStorage.beta_eq {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {j k : Fin s} (hk : ↑j + 1 = ↑k) (m : Fin s) : ls.beta m j = if m = j then ls.B j else ls.A k * ls.beta m k

The one-step recurrence of the slope weights in the second index: β_{m,j} = A_{j+1} β_{m,j+1} off the diagonal.

def BSeries.RungeKutta.LowStorage.toRK {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : RungeKutta (Fin s) R

The Butcher tableau induced by unrolling the Williamson recurrence: a_{ij} = Σ_{m<i} β_{m,j} and b_j = Σ_m β_{m,j}.

Equations

• ls.toRK = { A := fun (i j : Fin s) => ∑ m ∈ Finset.Iio i, ls.beta m j, b := fun (j : Fin s) => ∑ m : Fin s, ls.beta m j }

theorem BSeries.RungeKutta.LowStorage.toRK_A {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (i j : Fin s) : ls.toRK.A i j = ∑ m ∈ Finset.Iio i, ls.beta m j

theorem BSeries.RungeKutta.LowStorage.toRK_b {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (j : Fin s) : ls.toRK.b j = ∑ m : Fin s, ls.beta m j

theorem BSeries.RungeKutta.LowStorage.toRK_A_of_le {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {i j : Fin s} (hij : i ≤ j) : ls.toRK.A i j = 0

The induced tableau is strictly lower triangular.

theorem BSeries.RungeKutta.LowStorage.isExplicit_toRK {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : ls.toRK.IsExplicit

The induced tableau is explicit.

theorem BSeries.RungeKutta.LowStorage.toRK_b_succ {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {j k : Fin s} (hk : ↑j + 1 = ↑k) : ls.toRK.b j = ls.B j + ls.A k * ls.toRK.b k

The recurrence of the induced weights: b_j = B_j + A_{j+1} b_{j+1}.

theorem BSeries.RungeKutta.LowStorage.toRK_A_of_lt {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {i j k : Fin s} (hk : ↑j + 1 = ↑k) (hji : j < i) : ls.toRK.A i j = ls.B j + ls.A k * ls.toRK.A i k

The recurrence of the induced stage matrix: a_{ij} = B_j + A_{j+1} a_{i,j+1} for j < i.

theorem BSeries.RungeKutta.LowStorage.toRK_A_succ_self {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) {j k : Fin s} (hk : ↑j + 1 = ↑k) : ls.toRK.A k j = ls.B j

The subdiagonal of the induced tableau recovers the B coefficients: a_{j+1,j} = B_j.

def BSeries.RungeKutta.LowStorage.materialize {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : LowStorage s R

Materialise low-storage data: coefficients are computed once and stored as lists, so repeated access does not re-evaluate expensive coefficient expressions.

Equations

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

theorem BSeries.RungeKutta.LowStorage.materialize_eq {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : ls.materialize = ls

theorem BSeries.RungeKutta.LowStorage.toRK_b_last {R : Type v} {n : ℕ} [CommRing R] (ls : LowStorage (n + 1) R) : ls.toRK.b (Fin.last n) = ls.B (Fin.last n)

The last induced weight is B_{s-1}.

def BSeries.RungeKutta.IsWilliamson2N {R : Type v} [CommRing R] {s : ℕ} (rk : RungeKutta (Fin s) R) : Prop

A tableau is Williamson 2N if it arises from a two-register low-storage recurrence (arXiv:2509.20599, equation (2)).

Equations

• rk.IsWilliamson2N = ∃ (ls : BSeries.RungeKutta.LowStorage s R), ls.toRK = rk

def BSeries.RungeKutta.BazavovCondition {R : Type v} [CommRing R] {s : ℕ} (rk : RungeKutta (Fin s) R) : Prop

Bazavov's compatibility condition (arXiv:2509.20599, Theorem 3.1): a_{ik} (b_j - a_{kj}) = (a_{ij} - a_{kj}) b_k whenever k = j + 1 ≤ i.

Equations

• rk.BazavovCondition = ∀ (i j k : Fin s), ↑j + 1 = ↑k → k ≤ i → rk.A i k * (rk.b j - rk.A k j) = (rk.A i j - rk.A k j) * rk.b k

theorem BSeries.RungeKutta.IsWilliamson2N.bazavovCondition {R : Type v} [CommRing R] {s : ℕ} {rk : RungeKutta (Fin s) R} (h : rk.IsWilliamson2N) : rk.BazavovCondition

Williamson 2N tableaux satisfy Bazavov's condition (the forward direction of arXiv:2509.20599, Theorem 3.1).

def BSeries.RungeKutta.LowStorage.ofTableau {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) : LowStorage (n + 1) R

Reconstruct low-storage data from an explicit tableau: B_j = a_{j+1,j} (with B_{s-1} = b_{s-1}) and A_{j+1} = (b_j - a_{j+1,j}) / b_{j+1}.

Equations

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

theorem BSeries.RungeKutta.LowStorage.ofTableau_B {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) (j : Fin (n + 1)) : (ofTableau rk).B j = if h : ↑j + 1 < n + 1 then rk.A ⟨↑j + 1, h⟩ j else rk.b j

theorem BSeries.RungeKutta.LowStorage.ofTableau_A {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) (k : Fin (n + 1)) : (ofTableau rk).A k = if h : 0 < ↑k then (rk.b ⟨↑k - 1, ⋯⟩ - rk.A k ⟨↑k - 1, ⋯⟩) / rk.b k else 0

theorem BSeries.RungeKutta.LowStorage.ofTableau_B_of_succ {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) {j k : Fin (n + 1)} (hk : ↑j + 1 = ↑k) : (ofTableau rk).B j = rk.A k j

theorem BSeries.RungeKutta.LowStorage.ofTableau_B_last {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) : (ofTableau rk).B (Fin.last n) = rk.b (Fin.last n)

theorem BSeries.RungeKutta.LowStorage.ofTableau_A_of_succ {R : Type v} {n : ℕ} [Field R] (rk : RungeKutta (Fin (n + 1)) R) {j k : Fin (n + 1)} (hk : ↑j + 1 = ↑k) : (ofTableau rk).A k = (rk.b j - rk.A k j) / rk.b k

theorem BSeries.RungeKutta.isWilliamson2N_of_bazavovCondition {R : Type v} [Field R] {n : ℕ} {rk : RungeKutta (Fin (n + 1)) R} (hexp : rk.IsExplicit) (hb : ∀ (j : Fin (n + 1)), rk.b j ≠ 0) (hbaz : rk.BazavovCondition) : rk.IsWilliamson2N

Bazavov's theorem, converse direction (arXiv:2509.20599, Theorem 3.1): an explicit tableau with nonvanishing weights satisfying the compatibility condition is Williamson 2N.

theorem BSeries.RungeKutta.isWilliamson2N_iff_bazavovCondition {R : Type v} [Field R] {n : ℕ} {rk : RungeKutta (Fin (n + 1)) R} (hexp : rk.IsExplicit) (hb : ∀ (j : Fin (n + 1)), rk.b j ≠ 0) : rk.IsWilliamson2N ↔ rk.BazavovCondition

Bazavov's characterisation of Williamson 2N schemes (arXiv:2509.20599, Theorem 3.1; Bazavov, Theorem 2): an explicit tableau with nonvanishing weights is Williamson 2N if and only if it satisfies the compatibility condition.

Bazavov's commutator-free lift

A Williamson 2N scheme lifts to a commutator-free method by replacing the register update Y_l = Y_{l-1} + B_l δ_l with the exponential action Y_l = Λ(exp(B_l δ_l), Y_{l-1}) (arXiv:2509.20599, equation (4)). Unrolling the recurrence, the l-th exponential argument is V_l = Σ_j β_{l,j} K_j.

noncomputable def BSeries.RungeKutta.LowStorage.toCommutatorFree {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : CommutatorFreeMethod (Fin s) R

Bazavov's commutator-free lift of a Williamson 2N scheme (arXiv:2509.20599, equation (4)): stage i composes the exponentials exp(V_m) for m < i, where V_m = Σ_j β_{m,j} K_j, and the step composes all s of them. Each stage adds exactly one new exponential, so the lift uses s exponentials per step in two registers.

Equations

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

theorem BSeries.RungeKutta.LowStorage.toCommutatorFree_stageExps {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) (i : Fin s) : ls.toCommutatorFree.stageExps i = List.map (fun (m : Fin s) => ls.beta m) (List.filter (fun (m : Fin s) => decide (m < i)) (List.finRange s))

theorem BSeries.RungeKutta.LowStorage.toCommutatorFree_stepExps {R : Type v} {s : ℕ} [CommRing R] (ls : LowStorage s R) : ls.toCommutatorFree.stepExps = List.map (fun (m : Fin s) => ls.beta m) (List.finRange s)

def BSeries.ExponentialAction.translation (E : Type w) [AddCommMonoid E] : ExponentialAction E E

The translation action of a module on itself: the "flat" exponential map, under which commutator-free methods collapse to classical Runge–Kutta schemes.

Equations

• BSeries.ExponentialAction.translation E = { act := fun (a y : E) => y + a, act_zero := ⋯ }

theorem BSeries.ExponentialAction.applyList_translation {E : Type w} [AddCommMonoid E] (as : List E) (y : E) : (translation E).applyList as y = y + as.sum

theorem BSeries.RungeKutta.LowStorage.toCommutatorFree_stagePoint_translation {R : Type v} {s : ℕ} [CommRing R] {E : Type w} [AddCommMonoid E] [Module R E] (ls : LowStorage s R) (K : Fin s → E) (i : Fin s) (y : E) : ls.toCommutatorFree.stagePoint (ExponentialAction.translation E) K i y = y + ∑ j : Fin s, ls.toRK.A i j • K j

On a flat space the Bazavov lift reproduces the Runge–Kutta stage values: composing the lift's stage exponentials under the translation action yields the stage point of the induced Butcher tableau.

theorem BSeries.RungeKutta.LowStorage.toCommutatorFree_step_translation {R : Type v} {s : ℕ} [CommRing R] {E : Type w} [AddCommMonoid E] [Module R E] (ls : LowStorage s R) (K : Fin s → E) (y : E) : ls.toCommutatorFree.step (ExponentialAction.translation E) K y = y + ∑ j : Fin s, ls.toRK.b j • K j

On a flat space the Bazavov lift collapses to the classical Runge–Kutta step (arXiv:2509.20599, Section 3): the commutator-free step under the translation action is y + Σ_j b_j K_j for the induced Butcher weights.