Documentation

BSeries.Numerics.AntisymCriterion

The composed-weights criterion for antisymmetric order #

The master reduction turning the antisymmetric-order conditions of a Runge–Kutta scheme (arXiv:2507.21006, Section 8) into finite tableau arithmetic: a scheme has antisymmetric order at least m iff the elementary weights of the composed tableaux rk ∘ rk and rk* ∘ rk agree on all planar trees of order at most m.

We also record the classification of rooted trees of order at most two, used to turn the order-two conditions into the two weight identities Σ b = 1 and Σ b c = 1/2.

source
theorem BSeries.RootedTree.eq_bullet_of_order_one {τ : HopfAlgebras.RootedTree} (h : τ.order = 1) :
τ = HopfAlgebras.RootedTree.bullet

The unique tree of order one is the one-node tree.

source
theorem BSeries.RootedTree.forest_eq_of_order_one {ρ : HopfAlgebras.RootedForest} (h : ρ.order = 1) :
ρ = HopfAlgebras.RootedForest.singleton HopfAlgebras.RootedTree.bullet

Order-one forests are the singleton one-node tree.

source
theorem BSeries.RootedTree.eq_chain_of_order_two {τ : HopfAlgebras.RootedTree} (h : τ.order = 2) :
τ = (HopfAlgebras.RootedForest.singleton HopfAlgebras.RootedTree.bullet).graft

The unique tree of order two is the two-chain.

source
theorem BSeries.RungeKutta.graft_singleton_bullet :
(HopfAlgebras.RootedForest.singleton HopfAlgebras.RootedTree.bullet).graft = HopfAlgebras.RootedTree.ofPTree (HopfAlgebras.PTree.node [HopfAlgebras.PTree.node []])

The two-chain rooted tree in PTree form.

source
theorem BSeries.RungeKutta.hasAntisymOrder_iff_weight_compose_eq {ι : Type} [Fintype ι] {R : Type} [Field R] [CharZero R] [Invertible 2] (rk : RungeKutta ι R) (m : ℕ) :
ForestAlgebra.Character.HasAntisymOrder rk.series.toCharacter m ↔ ∀ (t : HopfAlgebras.PTree), t.order ≤ m → (rk.compose rk).weight t = (rk.adjointScheme.compose rk).weight t

The composed-weights criterion for antisymmetric order: by the SC ⟺ EC theorem, a Runge–Kutta method has antisymmetric order at least m iff the elementary weights of the two composed tableaux rk ∘ rk and rk* ∘ rk agree on all planar trees of order at most m — no coproducts or antipodes required (arXiv:2507.21006, Section 8).

source
@[implicit_reducible]
instance BSeries.RungeKutta.instInvertibleRatOfNat :
Invertible 2
Equations