Density of explicit Runge–Kutta methods

Butcher's Theorem 317A holds with the methods restricted to explicit tableaux (Butcher, Numerical Methods for ODEs, Remark after Theorem 317A; arXiv:2507.21006, Remark rmk:explicit_rk_density): all four constructions of the density proof — the zero scheme, block-diagonal sums, weight scalings, tableau scalings, and the one-stage extension — preserve strict lower-triangularity with respect to the lexicographic stage orders.

theorem BSeries.RungeKutta.isExplicit_zeroScheme {R : Type w} [Zero R] : (zeroScheme R).IsExplicit

theorem BSeries.RungeKutta.isExplicit_dirSum {ι : Type u} {κ : Type v} {R : Type w} [LinearOrder ι] [LinearOrder κ] [Zero R] {rk₁ : RungeKutta ι R} {rk₂ : RungeKutta κ R} (h₁ : rk₁.IsExplicit) (h₂ : rk₂.IsExplicit) : (rk₁.dirSum rk₂).IsExplicit

theorem BSeries.RungeKutta.isExplicit_scaleWeights {ι : Type u} {R : Type w} [LinearOrder ι] [Mul R] [Zero R] (c : R) {rk : RungeKutta ι R} (h : rk.IsExplicit) : (scaleWeights c rk).IsExplicit

theorem BSeries.RungeKutta.isExplicit_smulScheme {ι : Type u} {R : Type w} [LinearOrder ι] [MulZeroClass R] (c : R) {rk : RungeKutta ι R} (h : rk.IsExplicit) : (smulScheme c rk).IsExplicit

theorem BSeries.RungeKutta.isExplicit_extendScheme {ι : Type u} {R : Type w} [LinearOrder ι] [Zero R] [One R] {rk : RungeKutta ι R} (h : rk.IsExplicit) : rk.extendScheme.IsExplicit

def BSeries.RungeKutta.AchievableWeightsE {R : Type w} [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) (w : ↥T₀ → R) : Prop

A vector of prescribed elementary weights is explicitly achievable if some explicit Runge–Kutta method realizes it.

Equations

• BSeries.RungeKutta.AchievableWeightsE T₀ w = ∃ (ι : Type) (x : LinearOrder ι) (x_1 : Fintype ι) (rk : BSeries.RungeKutta ι R), rk.IsExplicit ∧ ∀ (t : ↥T₀), rk.treeWeight ↑t = w t

theorem BSeries.RungeKutta.achievableWeightsE_zero {R : Type w} [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) : AchievableWeightsE T₀ 0

theorem BSeries.RungeKutta.AchievableWeightsE.add {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w₁ w₂ : ↥T₀ → R} (h₁ : AchievableWeightsE T₀ w₁) (h₂ : AchievableWeightsE T₀ w₂) : AchievableWeightsE T₀ (w₁ + w₂)

theorem BSeries.RungeKutta.AchievableWeightsE.smul {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w : ↥T₀ → R} (c : R) (h : AchievableWeightsE T₀ w) : AchievableWeightsE T₀ (c • w)

theorem BSeries.RungeKutta.AchievableWeightsE.graded {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w : ↥T₀ → R} (c : R) (h : AchievableWeightsE T₀ w) : AchievableWeightsE T₀ fun (t : ↥T₀) => c ^ (↑t).order * w t

def BSeries.RungeKutta.achievableSubmoduleE (R : Type w) [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) : Submodule R (↥T₀ → R)

The explicitly achievable weight vectors form a submodule.

Equations

• BSeries.RungeKutta.achievableSubmoduleE R T₀ = { carrier := {w : ↥T₀ → R | BSeries.RungeKutta.AchievableWeightsE T₀ w}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem BSeries.RungeKutta.annihilator_gradedE {R : Type w} [Field R] [Infinite R] {T₀ : Finset HopfAlgebras.RootedTree} (ξ : ↥T₀ → R) (h : ∀ (w : ↥T₀ → R), AchievableWeightsE T₀ w → ∑ t : ↥T₀, ξ t * w t = 0) (d : ℕ) {w : ↥T₀ → R} (hw : AchievableWeightsE T₀ w) : ∑ t : ↥T₀ with (↑t).order = d, ξ t * w t = 0

Graded annihilation, explicit version.

theorem BSeries.RungeKutta.exists_explicit_rk_treeWeight {R : Type w} [Field R] [Infinite R] (n : ℕ) (T₀ : Finset HopfAlgebras.RootedTree) : T₀.sup HopfAlgebras.RootedTree.order ≤ n → ∀ (β : HopfAlgebras.RootedTree → R), AchievableWeightsE T₀ fun (t : ↥T₀) => β ↑t

Density of explicit Runge–Kutta methods (Butcher, Theorem 317A with the explicitness remark; arXiv:2507.21006, rmk:explicit_rk_density): any finite prescription of elementary weights is realized by an explicit Runge–Kutta method.

theorem BSeries.RungeKutta.exists_explicit_rk_forall_treeWeight {R : Type w} [Field R] [Infinite R] (T₀ : Finset HopfAlgebras.RootedTree) (β : HopfAlgebras.RootedTree → R) : ∃ (ι : Type) (x : LinearOrder ι) (x_1 : Fintype ι) (rk : RungeKutta ι R), rk.IsExplicit ∧ ∀ t ∈ T₀, rk.treeWeight t = β t

Explicit density, packaged for arbitrary finite tree sets.