Stage relabelling and the antisymmetric two-stage family

Relabelling the stages of a Runge–Kutta tableau leaves all elementary weights unchanged (P-equivalence; Butcher, Numerical Methods for ODEs, Theorem 381H). As an application we construct the antisymmetric two-stage family Ω_λ of arXiv:2507.21006, Section 7 — the tableau

A = [λ λ; -λ -λ], b = (λ, -λ) —

whose negation is a stage swap of itself, so its character is even.

def BSeries.RungeKutta.reindex {ι : Type u} {κ : Type v} {R : Type w} (e : κ ≃ ι) (rk : RungeKutta ι R) : RungeKutta κ R

Relabel the stages of a tableau along an equivalence.

Equations

• BSeries.RungeKutta.reindex e rk = { A := fun (i j : κ) => rk.A (e i) (e j), b := fun (j : κ) => rk.b (e j) }

theorem BSeries.RungeKutta.stageWeight_reindex {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (e : κ ≃ ι) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (i : κ) : (reindex e rk).stageWeight t i = rk.stageWeight t (e i)

theorem BSeries.RungeKutta.stageWeightList_reindex {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (e : κ ≃ ι) (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : κ) : (reindex e rk).stageWeightList ts i = rk.stageWeightList ts (e i)

theorem BSeries.RungeKutta.weight_reindex {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (e : κ ≃ ι) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) : (reindex e rk).weight t = rk.weight t

Stage relabelling preserves the elementary weights (P-equivalence; Butcher, Theorem 381H).

theorem BSeries.RungeKutta.treeWeight_reindex {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (e : κ ≃ ι) (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : (reindex e rk).treeWeight τ = rk.treeWeight τ

def BSeries.RungeKutta.boolSwap : Bool ≃ Bool

The stage swap of a two-stage scheme.

Equations

• BSeries.RungeKutta.boolSwap = { toFun := not, invFun := not, left_inv := Bool.not_not, right_inv := Bool.not_not }

def BSeries.RungeKutta.antisymScheme {R : Type w} [CommRing R] (l : R) : RungeKutta Bool R

The antisymmetric two-stage tableau Ω_λ of arXiv:2507.21006, Section 7: A = [λ λ; -λ -λ], b = (λ, -λ).

Equations

• BSeries.RungeKutta.antisymScheme l = { A := fun (i x : Bool) => if i = true then -l else l, b := fun (j : Bool) => if j = true then -l else l }

theorem BSeries.RungeKutta.negScheme_antisymScheme {R : Type w} [CommRing R] (l : R) : (antisymScheme l).negScheme = reindex boolSwap (antisymScheme l)

Negating Ω_λ is exactly the swap of its two stages.

theorem BSeries.RungeKutta.isEven_toCharacter_antisymScheme {R : Type w} [CommRing R] (l : R) : ForestAlgebra.Character.IsEven (antisymScheme l).series.toCharacter

The antisymmetric family is even: the character of Ω_λ is fixed by the canonical involution (arXiv:2507.21006, Section 7).

theorem BSeries.RungeKutta.weightBullet_antisymScheme {R : Type w} [CommRing R] (l : R) : (antisymScheme l).weight HopfAlgebras.PTree.bullet = 0

The quadrature weights of Ω_λ sum to zero: Ω_λ is inconsistent (a "do-nothing to first order" scheme).

theorem BSeries.RungeKutta.weight_chain2_antisymScheme {R : Type w} [CommRing R] (l : R) : (antisymScheme l).weight (HopfAlgebras.PTree.node [HopfAlgebras.PTree.node []]) = 4 * l ^ 2

The elementary weight of the two-chain detects λ: ω_λ(chain₂) = 4λ².