Documentation

BSeries.LieButcher.CFEESOrder

Lie–Butcher order theorems for CF-EES(2,5;x) and CF-EES(2,7;x) #

The order theorems of arXiv:2509.20599, Theorems E.1 and E.2, for the commutator-free lifts of the parametric EES families, verified at the generic parameter: over the computable rational-function fields CRatFunc ℚ and CRatFunc Qsqrt2 the planar order and antisymmetric order conditions become identities of rational functions in the family parameter, checked by native_decide through the memoised evaluator LowStorage.fastMethodChar.

The symbolic character values are cross-validated against Table 6 of arXiv:2509.20599: e.g. on the planar cherry the CF-EES(2,5;x) character equals (2x-5)/(32(x-1)) as a rational function.

This file is a leaf module so that the native evaluations never block edits to the general theory.

CF-EES(2,5;X): Theorem E.1 at the generic parameter #

source
def BSeries.RungeKutta.ees25Xls :
LowStorage 3 (CRatFunc ℚ)

The materialised generic low-storage data of EES(2,5;X) (top-level constant: evaluated once per process).

Equations
Instances For
    source
    theorem BSeries.RungeKutta.methodChar_cfEES25_cherry_generic :
    (ees25LowStorage CRatFunc.X).methodChar [HopfAlgebras.PTree.cherry] = (2 * CRatFunc.X - 5) / (32 * (CRatFunc.X - 1))

    Cross-validation against arXiv:2509.20599, Table 6, as an identity of rational functions: on the planar cherry the CF-EES(2,5;x) character equals (2x-5)/(32(x-1)).

    source
    theorem BSeries.RungeKutta.methodChar_cfEES25_chain3_generic :
    (ees25LowStorage CRatFunc.X).methodChar [HopfAlgebras.PTree.chain3] = 1 / 8

    Cross-validation against arXiv:2509.20599, Table 6: on the three-chain the character equals 1/8, independently of the parameter.

    source
    theorem BSeries.RungeKutta.hasPlanarOrder_two_cfEES25_generic :
    (ees25LowStorage CRatFunc.X).methodChar.HasPlanarOrder 2

    CF-EES(2,5;X) has planar order two at the generic parameter (arXiv:2509.20599, Theorem E.1(1)); this is an instance of the symbolic statement hasPlanarOrder_two_cfEES25.

    source
    theorem BSeries.RungeKutta.not_hasPlanarOrder_three_cfEES25_generic :
    ¬(ees25LowStorage CRatFunc.X).methodChar.HasPlanarOrder 3

    CF-EES(2,5;X) does not have planar order three: the cherry value (2X-5)/(32(X-1)) differs from 1/3 as a rational function.

    source
    theorem BSeries.RungeKutta.hasPlanarAntisymOrder_five_cfEES25_generic :
    (ees25LowStorage CRatFunc.X).methodChar.HasPlanarAntisymOrder 5

    CF-EES(2,5;X) has antisymmetric order five at the generic parameter (arXiv:2509.20599, Theorem E.1(2)): the symmetric defect of its LB character vanishes on all planar trees of order at most five, as identities of rational functions in the parameter.

    source
    theorem BSeries.RungeKutta.not_hasPlanarAntisymOrder_six_cfEES25_generic :
    ¬(ees25LowStorage CRatFunc.X).methodChar.HasPlanarAntisymOrder 6

    CF-EES(2,5;X) does not have antisymmetric order six: the six-chain is a witness at the generic parameter.

    CF-EES(2,7;(2-√2)/4): Theorem E.2 at the representative #

    source
    theorem BSeries.RungeKutta.hasPlanarOrder_two_cfEES27 :
    (ees27LowStorage Qsqrt2.sqrt2 x27).methodChar.HasPlanarOrder 2

    CF-EES(2,7;(2-√2)/4) has planar order two (arXiv:2509.20599, Theorem E.2).

    source
    theorem BSeries.RungeKutta.not_hasPlanarOrder_three_cfEES27 :
    ¬(ees27LowStorage Qsqrt2.sqrt2 x27).methodChar.HasPlanarOrder 3

    CF-EES(2,7;(2-√2)/4) does not have planar order three.

    source
    theorem BSeries.RungeKutta.hasPlanarAntisymOrder_seven_cfEES27 :
    (ees27LowStorage Qsqrt2.sqrt2 x27).methodChar.HasPlanarAntisymOrder 7

    CF-EES(2,7;(2-√2)/4) has antisymmetric order seven (arXiv:2509.20599, Theorem E.2): the symmetric defect of its LB character vanishes on all 197 planar trees of order at most seven.

    source
    theorem BSeries.RungeKutta.not_hasPlanarAntisymOrder_eight_cfEES27 :
    ¬(ees27LowStorage Qsqrt2.sqrt2 x27).methodChar.HasPlanarAntisymOrder 8

    CF-EES(2,7;(2-√2)/4) does not have antisymmetric order eight.