Documentation

BSeries.LieButcher.CommutatorFreeOrder

Lie–Butcher characters of 2N commutator-free methods #

The Bazavov lift of a Williamson 2N low-storage scheme advances by composing exponentials exp(V_e) with V_e = Σ_{i} β_{e,i} K_i, where K_i = ξ(Y_i) is the vector field frozen at the i-th stage point. Its Lie–Butcher character on planar forests is built by Owren's pseudo-stage substitution recursion (arXiv:2509.20599, Appendix E.2; Owren, Order conditions for commutator-free Lie group methods, Theorem 2.5):

The method character is ϕ = u_s. We formalise the planar order and antisymmetric order conditions of arXiv:2509.20599, Theorem E.1, and machine-check them for the concrete CF-EES(2,5;1/4) integrator, cross-validating the character values against Table 6 of the paper.

def BSeries.LSSeries.HasPlanarOrder {R : Type u} [Field R] (φ : LSSeries R) (p : ) :

An LB character has planar order p if it matches the exact-flow coefficients 1/τ! on every planar tree of order at most p (arXiv:2509.20599, Theorem E.1(1)).

Equations
Instances For

    The symmetric defect of an LB character: the Grossman–Larson composition of the grading-signed character with the character itself — the LB character of the roundtrip Φ_{-h} ∘ Φ_h (arXiv:2509.20599, Theorem E.1(2)).

    Equations
    Instances For

      An LB character has antisymmetric order m if its symmetric defect vanishes on every planar tree of order at most m: the roundtrip Φ_{-h} ∘ Φ_h recovers the identity to order m.

      Equations
      Instances For
        @[irreducible]

        The Lie–Butcher flow character u_e after e exponentials of the Bazavov commutator-free lift (Owren's substitution recursion; arXiv:2509.20599, Appendix E.2, equation (18)): u_0 = ε and

        u_{e+1}(ω) = Σ_{ω = ω₁ω₂} u_e(ω₁) ⋅ (1/|ω₂|!) ∏_{τ ∈ ω₂} V_e(τ),

        where V_e(τ) = Σ_i β_{e,i} u_i(children τ) combines the vector fields frozen at the stage points.

        Equations
        Instances For

          The Lie–Butcher character of the commutator-free method induced by a low-storage scheme: the flow character after all s exponentials (arXiv:2509.20599, Appendix E.2, equation (19)).

          Equations
          Instances For
            @[simp]
            theorem BSeries.RungeKutta.LowStorage.flowChar_nil {R : Type u} [Field R] {s : } (ls : LowStorage s R) (e : ) :
            ls.flowChar e [] = 1

            Every flow character takes the value one on the empty forest.

            @[simp]
            theorem BSeries.RungeKutta.LowStorage.flowChar_bullet {R : Type u} [Field R] {s : } (ls : LowStorage s R) (e : ) :
            ls.flowChar e [HopfAlgebras.PTree.bullet] = (List.map (fun (m : ) => (List.map (fun (i : ) => if h : m < s i < s then ls.beta m, i, else 0) (List.range s)).sum) (List.range e)).sum

            The flow character on the single-node forest accumulates the row sums of the slope weights: u_e([•]) = Σ_{m<e} Σ_i β_{m,i}.

            Consistency of the Lie–Butcher character: on the single-node tree the method character of the commutator-free lift equals the sum of the induced quadrature weights Σⱼ bⱼ.

            The flow character on trees of order at most two #

            In general the method character reproduces the Runge–Kutta elementary weights of the induced tableau on the bullet and the two-chain, which yields the planar order-two condition for a whole family at once.

            The flow character on the single bullet is the partial abscissa: for i < s, u_i([•]) = c_i, the i-th row sum of the induced tableau.

            theorem BSeries.RungeKutta.LowStorage.flowChar_chain2 {R : Type u} [Field R] {s : } (ls : LowStorage s R) (e : ) :
            ls.flowChar e [HopfAlgebras.PTree.chain2] = (List.map (fun (m : ) => (List.map (fun (i : ) => (if h : m < s i < s then ls.beta m, i, else 0) * ls.flowChar i [HopfAlgebras.PTree.bullet]) (List.range s)).sum) (List.range e)).sum

            The flow character on the two-chain accumulates the slope weights against the bullet values.

            The Lie–Butcher character matches the Runge–Kutta weight on the two-chain: ϕ(chain₂) = Σᵢ bᵢ cᵢ for the induced tableau.

            A memoised evaluator #

            flowChar recomputes stage characters exponentially often along deep trees. For machine-checked order conditions we use an equivalent evaluator that annotates each tree once with its slope values [u_0(children τ), …, u_{s-1}(children τ)] and never re-descends into trees, making character evaluation polynomial in the forest order.

            The slope values of a tree, as data: trueSlopes τ = [u_0(children τ), …, u_{s-1}(children τ)].

            Equations
            Instances For
              def BSeries.RungeKutta.LowStorage.flowCharAnn {R : Type u} [Field R] {s : } (ls : LowStorage s R) :
              List (List R)R

              The flow character evaluated on a forest of precomputed slope-value lists: the recursion never re-enters the trees.

              Equations
              Instances For
                @[irreducible]

                The memoised slope annotation: each subtree's slope list is computed exactly once.

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

                  The memoised method character.

                  Equations
                  Instances For

                    The memoised evaluator computes the method character. All machine-checked order conditions evaluate fastMethodChar instead of the exponential-time methodChar recursion.

                    Planar order two from the induced tableau #

                    The only planar tree of order one is the bullet.

                    The only planar tree of order two is the two-chain.

                    theorem BSeries.RungeKutta.hasPlanarOrder_two_of_toRK {R : Type u} [Field R] {s : } (ls : LowStorage s R) (h1 : j : Fin s, ls.toRK.b j = 1) (h2 : i : Fin s, ls.toRK.b i * ls.toRK.abscissa i = 1 / 2) :

                    Planar order two from the induced tableau weights: if the induced Butcher tableau of a low-storage scheme is consistent (Σⱼ bⱼ = 1) and satisfies the classical order-two condition (Σᵢ bᵢcᵢ = 1/2), then the commutator-free lift has planar order two on any homogeneous space.

                    theorem BSeries.RungeKutta.hasPlanarOrder_two_cfEES25 {R : Type u} [Field R] {x : R} (hx1 : x 1) (hx2 : 2 * x 1) (hx3 : 2 * x -1) (h2 : 2 0) :

                    CF-EES(2,5;x) has planar order two for every admissible parameter (arXiv:2509.20599, Theorem E.1(1) in full generality): the Lie–Butcher character of the commutator-free lift of EES(2,5;x) matches the exact flow on all planar trees of order at most two, over any field of characteristic ≠ 2 and any x ∉ {1, ±1/2}.