Explicit and Effectively Symmetric (EES) Runge–Kutta schemes

Following arXiv:2507.21006, Section 8. The antisymmetric component of any B-series method vanishes on forests of odd order (Proposition 8.2, prop:plus_zero), so the antisymmetric order of a method is always odd or infinite; a method is symmetric precisely when its antisymmetric component is trivial at every order. An EES(n, m) scheme is an explicit Runge–Kutta scheme of order exactly n and antisymmetric order exactly m.

theorem BSeries.ForestAlgebra.Character.antisymmetricPart_evalForest_of_odd_order {R : Type u} [CommRing R] [Invertible 2] (ψ : HopfAlgebras.ForestAlgebra.Character R) {φ : HopfAlgebras.RootedForest} (hφ : Odd φ.order) : (antisymmetricPart ψ).evalForest φ = 0

The antisymmetric component vanishes at odd orders: τ⁺ = 0 for |τ| odd (arXiv:2507.21006, Proposition plus_zero), in functional form.

def BSeries.ForestAlgebra.Character.HasAntisymOrder {R : Type u} [CommRing R] [Invertible 2] (ψ : HopfAlgebras.ForestAlgebra.Character R) (m : ℕ) : Prop

A B-series method has antisymmetric order at least m if its antisymmetric component agrees with the counit on all forests of order at most m, i.e. ψ(τ⁺) = 0 for 1 ≤ |τ| ≤ m (arXiv:2507.21006, Definition 8.1).

Equations

• BSeries.ForestAlgebra.Character.HasAntisymOrder ψ m = (BSeries.ForestAlgebra.Character.antisymmetricPart ψ).AgreeUpToOrder (HopfAlgebras.ForestAlgebra.LinearFunctional.counit R) m

theorem BSeries.ForestAlgebra.Character.HasAntisymOrder.mono {R : Type u} [CommRing R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {k m : ℕ} (h : HasAntisymOrder ψ m) (hkm : k ≤ m) : HasAntisymOrder ψ k

theorem BSeries.ForestAlgebra.Character.HasAntisymOrder.succ_of_even {R : Type u} [CommRing R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {m : ℕ} (h : HasAntisymOrder ψ m) (hm : Even m) : HasAntisymOrder ψ (m + 1)

The antisymmetric order is odd (or infinite): since τ⁺ = 0 at odd orders, antisymmetric order at an even m extends automatically to m + 1 (arXiv:2507.21006, Section 8).

theorem BSeries.ForestAlgebra.Character.antisymmetricPart_of_isOdd {R : Type u} [CommRing R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} (h : IsOdd ψ) : antisymmetricPart ψ = HopfAlgebras.ForestAlgebra.LinearFunctional.counit R

An odd (symmetric) character has trivial antisymmetric component.

theorem BSeries.ForestAlgebra.Character.hasAntisymOrder_of_isOdd {R : Type u} [CommRing R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} (h : IsOdd ψ) (m : ℕ) : HasAntisymOrder ψ m

Symmetric methods have infinite antisymmetric order.

theorem BSeries.ForestAlgebra.Character.isOdd_of_forall_hasAntisymOrder {R : Type u} [CommRing R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} (h : ∀ (m : ℕ), HasAntisymOrder ψ m) : IsOdd ψ

A method with infinite antisymmetric order is symmetric.

theorem BSeries.ForestAlgebra.Character.isOdd_iff_forall_hasAntisymOrder {R : Type u} [CommRing R] [Invertible 2] (ψ : HopfAlgebras.ForestAlgebra.Character R) : IsOdd ψ ↔ ∀ (m : ℕ), HasAntisymOrder ψ m

A B-series method is symmetric iff its antisymmetric order is infinite (arXiv:2507.21006, Section 8).

def BSeries.RungeKutta.IsExplicit {ι : Type u} {R : Type v} [LinearOrder ι] [Zero R] (rk : RungeKutta ι R) : Prop

A Runge–Kutta tableau is explicit when its stage matrix is strictly lower triangular with respect to a linear order on the stages.

Equations

• rk.IsExplicit = ∀ (i j : ι), i ≤ j → rk.A i j = 0

theorem BSeries.RungeKutta.explicitEuler_isExplicit {R : Type v} [Zero R] [One R] : (explicitEuler R).IsExplicit

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

Composition preserves explicitness, ordering all first-block stages before the second block (lexicographic order on the stages).

def BSeries.RungeKutta.IsEES {ι : Type u} {R : Type v} [LinearOrder ι] [Fintype ι] [Field R] [Invertible 2] (rk : RungeKutta ι R) (n m : ℕ) : Prop

An Explicit and Effectively Symmetric scheme of order n and antisymmetric order m: an explicit Runge–Kutta scheme with ord(ψ) = n and ord⁺(ψ) = m (arXiv:2507.21006, Definition 8.2, the class EES(n, m)).

Equations

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

theorem BSeries.RungeKutta.IsEES.odd_antisymOrder {ι : Type u} {R : Type v} [LinearOrder ι] [Fintype ι] [Field R] [Invertible 2] {rk : RungeKutta ι R} {n m : ℕ} (h : rk.IsEES n m) : Odd m

The antisymmetric order of an EES scheme is odd (arXiv:2507.21006, Section 8): the class EES(n, m) is empty for even m.

theorem BSeries.ForestAlgebra.Character.hasAntisymOrder_of_agree_exact {R : Type w} [Field R] [CharZero R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → ψ.evalForest φ = (Series.exact R).toCharacter.evalForest φ) : HasAntisymOrder ψ n

The antisymmetric order dominates the order: a method agreeing with the exact solution up to order n has antisymmetric order at least n (arXiv:2507.21006, Section 8: ord⁺(ψ) ≥ ord(ψ)).

theorem BSeries.ForestAlgebra.Character.antisymmetricPart_eval_first_defect {R : Type w} [Field R] [CharZero R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {m : ℕ} (hm : Odd m) (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ m → ψ.evalForest φ = (Series.exact R).toCharacter.evalForest φ) {τ : HopfAlgebras.RootedForest} (hτ : τ.order = m + 1) : (antisymmetricPart ψ) (HopfAlgebras.ForestAlgebra.ofForest τ) = ψ.evalForest τ - (Series.exact R).toCharacter.evalForest τ

The antisymmetric component detects the leading defect at even orders: if ψ agrees with the exact solution up to an odd order m, then at order m + 1 the antisymmetric component equals the defect of ψ. Hence a method of order exactly m (m odd) has antisymmetric order exactly m (arXiv:2507.21006, Section 8).

theorem BSeries.ForestAlgebra.Character.sqrtCoeff_convolution_self {R : Type w} [Field R] [Invertible 2] (ψ : HopfAlgebras.ForestAlgebra.Character R) (φ : HopfAlgebras.RootedForest) : RootedForest.sqrtCoeff (ψ.convolution ψ) φ = ψ.evalForest φ

A character is its own square root's square: ψ = (ψ⋆ψ)^{1/2} pointwise.

theorem BSeries.ForestAlgebra.Character.hasAntisymOrder_iff_convolution_agree {R : Type w} [Field R] [CharZero R] [Invertible 2] (ψ : HopfAlgebras.ForestAlgebra.Character R) (m : ℕ) : HasAntisymOrder ψ m ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ m → (ψ.convolution ψ).evalForest φ = ((adjointCharacter ψ).convolution ψ).evalForest φ

Equivalence of the SC and EC order conditions (arXiv:2507.21006, Section 8): the antisymmetric order conditions ψ(τ⁺) = 0 up to order m hold iff the square-free conditions (ψ⋆ψ)(τ) = (ψ*⋆ψ)(τ) hold up to order m — a criterion involving only convolutions and the antipode, with no square roots.