Documentation

BSeries.Numerics.EES27

The EES(2,7;x) family #

The four-stage EES(2,7;x) Runge–Kutta family (arXiv:2507.21006, Section 8, positive √2 branch), over any field R with a chosen square root s of two. The Butcher tableau is

b = (x, (2-s)/2 - (1-s)x, (1-s)(x-1), (2-s)/2 - x)

with the stage matrix recorded below; the concrete representatives at x = (2-√2)/4 and x = (5-3√2)/14 of the paper arise by specialisation.

The order conditions are verified at the generic parameter: taking R := CRatFunc Qsqrt2, s := √2 and x := X an indeterminate, the conditions become identities of rational functions over ℚ(√2), checked by native_decide. In this sense the results hold for the whole family:

source
def BSeries.RungeKutta.ees27 {R : Type v} [Field R] (s x : R) :
RungeKutta (Fin 4) R

The four-stage EES(2,7;x) family (arXiv:2507.21006, Section 8, +√2 branch), over a field with a distinguished square root s of two: the stage matrix of the proposition, with α = (2x+s)/((2x-1)(1-s-2x)) and β = 1/((2x-1)(1-s-2x)(2-s-2x)).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BSeries.RungeKutta.isExplicit_ees27 {R : Type v} [Field R] (s x : R) :
    (ees27 s x).IsExplicit

    The family is explicit for all parameters: the strictly upper triangle of the stage matrix consists of literal zeros.

    source
    def BSeries.RungeKutta.ees27LowStorage {R : Type v} [Field R] (s x : R) :
    LowStorage 4 R

    The Williamson 2N coefficients of EES(2,7;x), read off the tableau (arXiv:2509.20599, Appendix D): B = (a₂₁, a₃₂, a₄₃, b₄) and A_{l+1} = (b_l - a_{l+1,l}) / b_{l+1} along the subdiagonal.

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

      The representative parameter x = (2-√2)/4 #

      Verifying the EES(2,7;x) order conditions symbolically in x is a heavy rational-function computation over ℚ(√2)(x); the machine-checked verification below is at the numerically simple representative x = (2-√2)/4 of arXiv:2507.21006, Section 8, over the computable field ℚ(√2). (The three-stage EES(2,5;x) family is verified at the generic parameter, in BSeries.Numerics.EES25.)

      source
      def BSeries.RungeKutta.x27 :
      Qsqrt2

      The representative parameter (2-√2)/4.

      Equations
      Instances For
        source
        def BSeries.RungeKutta.ees27r :
        RungeKutta (Fin 4) Qsqrt2

        The EES(2,7; (2-√2)/4) scheme, obtained from the family.

        Equations
        Instances For
          source
          theorem BSeries.RungeKutta.isExplicit_ees27r :
          ees27r.IsExplicit
          source
          def BSeries.RungeKutta.ees27rComp :
          RungeKutta (Fin 8) Qsqrt2

          The materialised composed tableau ees27r ∘ ees27r (top-level constant: entries are evaluated once per process).

          Equations
          Instances For
            source
            def BSeries.RungeKutta.ees27rAdj :
            RungeKutta (Fin 8) Qsqrt2

            The materialised composed tableau ees27r* ∘ ees27r.

            Equations
            Instances For
              source
              def BSeries.RungeKutta.ees27rLowStorage :
              LowStorage 4 Qsqrt2

              The materialised low-storage data at the representative.

              Equations
              Instances For
                source
                theorem BSeries.RungeKutta.hasOrder_two_ees27r :
                ees27r.HasOrder 2

                EES(2,7;(2-√2)/4) has order two (machine-checked).

                source
                theorem BSeries.RungeKutta.not_hasOrder_three_ees27r :
                ¬ees27r.HasOrder 3

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

                source
                theorem BSeries.RungeKutta.hasAntisymOrder_seven_ees27r :
                ForestAlgebra.Character.HasAntisymOrder ees27r.series.toCharacter 7

                EES(2,7;(2-√2)/4) has antisymmetric order seven (machine-checked composed-weight identities).

                source
                theorem BSeries.RungeKutta.not_hasAntisymOrder_eight_ees27r :
                ¬ForestAlgebra.Character.HasAntisymOrder ees27r.series.toCharacter 8

                EES(2,7;(2-√2)/4) does not have antisymmetric order eight: the eight-chain is a witness.

                source
                theorem BSeries.RungeKutta.isEES_ees27r :
                ees27r.IsEES 2 7

                EES(2,7;(2-√2)/4) is an EES(2,7) scheme (arXiv:2507.21006, Section 8): explicit, of order exactly two, with antisymmetric order exactly seven.

                source
                theorem BSeries.RungeKutta.isWilliamson2N_ees27r :
                ees27r.IsWilliamson2N

                EES(2,7;(2-√2)/4) is Williamson 2N (arXiv:2509.20599, Proposition 3.1): the two-register coefficients read off the tableau induce it back.