Construction of characters with prescribed exact orders

The two building blocks of the existence theorem for EES schemes (arXiv:2507.21006, Section 8): for every even n there is an odd character agreeing with the exact solution up to order n but not n + 1 (a symmetric method of order exactly n), and for every odd m there is an even character whose antisymmetric order is exactly m.

Both are obtained from Butcher's density theorem 317A: prescribe the elementary weights 1/τ! up to the target order and introduce a deliberate defect one order higher, then pass to the symmetric or antisymmetric component; the defect-transfer lemmas show the defect survives.

def BSeries.PTree.tallTree : ℕ → HopfAlgebras.PTree

The chain (tall) tree of order k + 1.

Equations

• BSeries.PTree.tallTree 0 = HopfAlgebras.PTree.node []
• BSeries.PTree.tallTree k.succ = HopfAlgebras.PTree.node [BSeries.PTree.tallTree k]

theorem BSeries.PTree.order_tallTree (k : ℕ) : (tallTree k).order = k + 1

theorem BSeries.ForestAlgebra.Character.exists_isOdd_agree_defect (R : Type w) [Field R] [CharZero R] [Invertible 2] {n : ℕ} (hn : Even n) : ∃ (φ : HopfAlgebras.ForestAlgebra.Character R), IsOdd φ ∧ (∀ (ρ : HopfAlgebras.RootedForest), ρ.order ≤ n → φ.evalForest ρ = (Series.exact R).toCharacter.evalForest ρ) ∧ ∃ (τ : HopfAlgebras.RootedForest), τ.order = n + 1 ∧ φ.evalForest τ ≠ (Series.exact R).toCharacter.evalForest τ

Symmetric methods of every even order exist, sharply: for even n there is an odd character agreeing with the exact solution up to order n and failing at order n + 1 (arXiv:2507.21006, Section 8).

theorem BSeries.ForestAlgebra.Character.exists_isEven_antisym_defect (R : Type w) [Field R] [CharZero R] [Invertible 2] {m : ℕ} (hm : Odd m) : ∃ (ζ : HopfAlgebras.ForestAlgebra.Character R), IsEven ζ ∧ (∀ (ρ : HopfAlgebras.RootedForest), ρ.order ≤ m → ζ.evalForest ρ = (HopfAlgebras.ForestAlgebra.LinearFunctional.counit R).evalForest ρ) ∧ ∃ (τ : HopfAlgebras.RootedForest), τ.order = m + 1 ∧ ζ.evalForest τ ≠ (HopfAlgebras.ForestAlgebra.LinearFunctional.counit R).evalForest τ

Even characters of every odd antisymmetric order exist, sharply: for odd m there is an even character whose antisymmetric component (which is itself) vanishes up to order m and fails at order m + 1 (arXiv:2507.21006, Section 8).

theorem BSeries.ForestAlgebra.Character.exists_character_ees_orders (R : Type w) [Field R] [CharZero R] [Invertible 2] {n m : ℕ} (hn : Even n) (hm : Odd m) (hnm : n < m) : ∃ (γ : HopfAlgebras.ForestAlgebra.Character R), (∀ (ρ : HopfAlgebras.RootedForest), ρ.order ≤ n → γ.evalForest ρ = (Series.exact R).toCharacter.evalForest ρ) ∧ (∃ (τ : HopfAlgebras.RootedForest), τ.order = n + 1 ∧ γ.evalForest τ ≠ (Series.exact R).toCharacter.evalForest τ) ∧ HasAntisymOrder γ m ∧ ¬HasAntisymOrder γ (m + 1)

Existence of EES characters (arXiv:2507.21006, Section 8, the core of the existence theorem): for even n and odd m > n there is a character of order exactly n whose antisymmetric order is exactly m, namely γ = ζ ⋆ φ for the constructed even ζ and odd φ.

theorem BSeries.ForestAlgebra.Character.evalForest_congr_of_tree_congr {R : Type w} [CommRing R] {χ ξ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → χ.evalForest (HopfAlgebras.RootedForest.singleton τ) = ξ.evalForest (HopfAlgebras.RootedForest.singleton τ)) (ρ : HopfAlgebras.RootedForest) : ρ.order ≤ n → χ.evalForest ρ = ξ.evalForest ρ

Characters agreeing on all trees of order at most n agree on all forests of order at most n (characters are multiplicative).

theorem BSeries.ForestAlgebra.Character.antisymmetricPart_evalForest_congr {R : Type w} [Field R] [Invertible 2] {χ ξ : HopfAlgebras.ForestAlgebra.Character R} {k : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ k → χ.evalForest φ = ξ.evalForest φ) (ρ : HopfAlgebras.RootedForest) : ρ.order ≤ k → (antisymmetricPart χ) (HopfAlgebras.ForestAlgebra.ofForest ρ) = (antisymmetricPart ξ) (HopfAlgebras.ForestAlgebra.ofForest ρ)

Order-agreement between two characters transports to their antisymmetric components.

theorem BSeries.ForestAlgebra.Character.exists_rk_ees_orders (R : Type w) [Field R] [CharZero R] [Invertible 2] {n m : ℕ} (hn : Even n) (hm : Odd m) (hnm : n < m) : ∃ (ι : Type) (x : Fintype ι) (rk : RungeKutta ι R), (rk.HasOrder n ∧ ¬rk.HasOrder (n + 1)) ∧ HasAntisymOrder rk.series.toCharacter m ∧ ¬HasAntisymOrder rk.series.toCharacter (m + 1)

Existence of Runge–Kutta methods with EES orders (arXiv:2507.21006, Section 8, Existence of EES Runge–Kutta Schemes, without the explicitness refinement): for every even n > 0 and odd m > n there is a Runge–Kutta method of order exactly n whose antisymmetric order is exactly m.

theorem BSeries.ForestAlgebra.Character.exists_isEES (R : Type w) [Field R] [CharZero R] [Invertible 2] {n m : ℕ} (hn : Even n) (hm : Odd m) (hnm : n < m) : ∃ (ι : Type) (x : LinearOrder ι) (x_1 : Fintype ι) (rk : RungeKutta ι R), rk.IsEES n m

Existence of EES Runge–Kutta schemes (arXiv:2507.21006, Section 8, Theorem "Existence of EES Runge–Kutta Schemes"): for every even n > 0 and every odd m > n there is an explicit Runge–Kutta scheme belonging to EES(n, m).

def BSeries.ForestAlgebra.Character.IsRKCharacter {R : Type w} [Field R] (χ : HopfAlgebras.ForestAlgebra.Character R) : Prop

A character realized by some Runge–Kutta method.

Equations

• BSeries.ForestAlgebra.Character.IsRKCharacter χ = ∃ (ι : Type) (x : Fintype ι) (rk : BSeries.RungeKutta ι R), χ = rk.series.toCharacter

def BSeries.ForestAlgebra.Character.IsConsistent {R : Type w} [Field R] (χ : HopfAlgebras.ForestAlgebra.Character R) : Prop

A consistent method: the first-order weight is 1.

Equations

• BSeries.ForestAlgebra.Character.IsConsistent χ = (χ.evalForest (HopfAlgebras.RootedForest.singleton HopfAlgebras.RootedTree.bullet) = 1)

theorem BSeries.ForestAlgebra.Character.infinite_consistent_rk_sEquiv (R : Type w) [Field R] [CharZero R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} (hRK : IsRKCharacter ψ) (hcons : IsConsistent ψ) : {χ : HopfAlgebras.ForestAlgebra.Character R | IsRKCharacter χ ∧ IsConsistent χ ∧ SEquiv χ ψ}.Infinite

S-equivalence classes contain 0 or infinitely many consistent Runge–Kutta characters (arXiv:2507.21006, Section 7, the infinitude half of the n theorem): if a class contains one consistent RK character, the antisymmetric family produces infinitely many.

theorem BSeries.ForestAlgebra.Character.not_isConsistent_of_sEquiv_unit {R : Type w} [Field R] [CharZero R] [Invertible 2] {χ : HopfAlgebras.ForestAlgebra.Character R} (h : SEquiv χ (HopfAlgebras.ForestAlgebra.Character.unit R)) : ¬IsConsistent χ

The zero value is attained: the S-equivalence class of the unit (the identity method, whose class is the even characters) contains no consistent character (arXiv:2507.21006, Section 7, the 0-half of the n theorem).