Runge–Kutta order conditions over rooted trees

A Runge–Kutta method with tableau (A, b) has order p when the elementary weight Φ(t)(A, b) equals 1/γ(t) for every rooted tree t with at most p nodes, where γ is the density (Butcher). This file builds a computable engine over planar rooted trees (order |t|, density γ(t), elementary weight Φ(t)(A, b)), states the order conditions in the division-free form γ(t) · Φ(t) = 1, reduces "order p" to a finite catalogue check, and certifies concrete methods.

Main results

• Butcher.satisfiesOrderConditions_iff: "order p" holds iff the condition holds on the finite catalogue of trees with at most p nodes (sound and complete).
• Butcher.euler_ord1, Butcher.heun_ord2, Butcher.heun_not_ord3: Euler has order 1, Heun order 2 and not 3.
• Butcher.rk4_order4, Butcher.rk4_not_ord5: the classical RK4 has order 4 and not 5.
• Butcher.dp_order5: Dormand–Prince (DOPRI5) has order 5.
• Butcher.gauss_order4: Gauss–Legendre with 3 stages has order 4, coefficients in ℚ(√15).
• Butcher.gauss_order6: the Gauss–Legendre tableau with 3 stages, cleared of denominators by D = 360 into ℤ[√15], satisfies γ(t) · Φ(D·A, D·b, t) = D^{|t|} for every tree with at most 6 nodes (by decide). The equivalence with the unscaled conditions (homogeneity of Φ) is not formalized.
• Butcher.orderCond_node_perm: Φ and γ are invariant under permuting a node's children, so the conditions on planar trees subsume those on abstract trees.

Implementation notes

Only the algebraic order conditions are certified, not Butcher's theorem that they are equivalent to a local error O(h^{p+1}). Trees are planar (ordered children), with their own inductive type Butcher.RTree, of the same shape as ConnesKreimer.RTree; Mathlib's order-theoretic RootedTree is not used (see Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Coproduct). Butcher.Q15 and Butcher.Z15 are computable models of ℚ(√15) and ℤ[√15] as pairs. Mathlib has Zsqrtd 15 and QuadraticAlgebra; the concrete pairs are kept because the certificates unfold them with simp and decide. Over ℚ the kernel cannot reduce the Nat.gcd inside Rat normalization, so the ℚ conditions are closed by norm_num and the order-6 certificate works over integers.

References

• J. C. Butcher, Coefficients for the study of Runge–Kutta integration processes, J. Austral. Math. Soc. 3 (1963) 185–201.
• E. Hairer, C. Lubich, G. Wanner, Geometric Numerical Integration, Springer (2006).
• L. Foissy, Les algèbres de Hopf des arbres enracinés décorés, I, Bull. Sci. Math. 126 (2002) 193–239.
• C. Marín, What Order a Method Knows: certified Runge–Kutta order conditions over rooted trees, machine-checked in Lean 4 (2026), doi:10.5281/zenodo.20787666. Ported from ButcherOrder.lean of karlesmarin/runge-kutta-order-conditions-lean (Lean v4.30.0-rc2).

structure Butcher.Q15 : Type

ℚ(√15) as a computable CommRing: ⟨a, b⟩ means a + b·√15; the relation √15²=15 is baked into mul. Coefficient ring for the Gauss–Legendre s=3 tableau (gauss_order4). Working in this concrete pair ring keeps the order-condition checks a pure ℚ component computation closed by norm_num — no algebraic-number tactic needed.

• re : ℚ
• im : ℚ

def Butcher.instDecidableEqQ15.decEq (x✝ x✝¹ : Q15) : Decidable (x✝ = x✝¹)

Equations

• Butcher.instDecidableEqQ15.decEq { re := a, im := a_1 } { re := b, im := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Butcher.instDecidableEqQ15 : DecidableEq Q15

Equations

• Butcher.instDecidableEqQ15 = Butcher.instDecidableEqQ15.decEq

def Butcher.instReprQ15.repr : Q15 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Butcher.instReprQ15 : Repr Q15

Equations

• Butcher.instReprQ15 = { reprPrec := Butcher.instReprQ15.repr }

theorem Butcher.Q15.ext' {x y : Q15} (hr : x.re = y.re) (hi : x.im = y.im) : x = y

theorem Butcher.Q15.ext'_iff {x y : Q15} : x = y ↔ x.re = y.re ∧ x.im = y.im

@[instance_reducible]

instance Butcher.Q15.instZero : Zero Q15

Equations

• Butcher.Q15.instZero = { zero := { re := 0, im := 0 } }

@[instance_reducible]

instance Butcher.Q15.instOne : One Q15

Equations

• Butcher.Q15.instOne = { one := { re := 1, im := 0 } }

@[instance_reducible]

instance Butcher.Q15.instAdd : Add Q15

Equations

• Butcher.Q15.instAdd = { add := fun (x y : Butcher.Q15) => { re := x.re + y.re, im := x.im + y.im } }

@[instance_reducible]

instance Butcher.Q15.instNeg : Neg Q15

Equations

• Butcher.Q15.instNeg = { neg := fun (x : Butcher.Q15) => { re := -x.re, im := -x.im } }

@[instance_reducible]

instance Butcher.Q15.instSub : Sub Q15

Equations

• Butcher.Q15.instSub = { sub := fun (x y : Butcher.Q15) => { re := x.re - y.re, im := x.im - y.im } }

@[instance_reducible]

instance Butcher.Q15.instMul : Mul Q15

Equations

• Butcher.Q15.instMul = { mul := fun (x y : Butcher.Q15) => { re := x.re * y.re + 15 * x.im * y.im, im := x.re * y.im + x.im * y.re } }

@[simp]

theorem Butcher.Q15.zero_re : re 0 = 0

@[simp]

theorem Butcher.Q15.zero_im : im 0 = 0

@[simp]

theorem Butcher.Q15.one_re : re 1 = 1

@[simp]

theorem Butcher.Q15.one_im : im 1 = 0

@[simp]

theorem Butcher.Q15.add_re (x y : Q15) : (x + y).re = x.re + y.re

@[simp]

theorem Butcher.Q15.add_im (x y : Q15) : (x + y).im = x.im + y.im

@[simp]

theorem Butcher.Q15.neg_re (x : Q15) : (-x).re = -x.re

@[simp]

theorem Butcher.Q15.neg_im (x : Q15) : (-x).im = -x.im

@[simp]

theorem Butcher.Q15.sub_re (x y : Q15) : (x - y).re = x.re - y.re

@[simp]

theorem Butcher.Q15.sub_im (x y : Q15) : (x - y).im = x.im - y.im

@[simp]

theorem Butcher.Q15.mul_re (x y : Q15) : (x * y).re = x.re * y.re + 15 * x.im * y.im

@[simp]

theorem Butcher.Q15.mul_im (x y : Q15) : (x * y).im = x.re * y.im + x.im * y.re

@[instance_reducible]

instance Butcher.Q15.instCommRing : CommRing Q15

Equations

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

@[simp]

theorem Butcher.Q15.natCast_eq (n : ℕ) : ↑n = { re := ↑n, im := 0 }

structure Butcher.Z15 : Type

ℤ[√15] as a computable CommRing: ⟨a,b⟩ means a + b·√15 with a,b : ℤ. Identical in shape to Q15 but over the INTEGERS, so equality is decided by the kernel's GMP Int arithmetic with no rational Nat.gcd normalization. Used in gauss_order6 to certify Gauss order 6 by decide after the tableau is cleared of denominators (scaled by D=360).

• re : ℤ
• im : ℤ

@[instance_reducible]

instance Butcher.instDecidableEqZ15 : DecidableEq Z15

Equations

• Butcher.instDecidableEqZ15 = Butcher.instDecidableEqZ15.decEq

def Butcher.instDecidableEqZ15.decEq (x✝ x✝¹ : Z15) : Decidable (x✝ = x✝¹)

Equations

• Butcher.instDecidableEqZ15.decEq { re := a, im := a_1 } { re := b, im := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Butcher.instReprZ15 : Repr Z15

Equations

• Butcher.instReprZ15 = { reprPrec := Butcher.instReprZ15.repr }

def Butcher.instReprZ15.repr : Z15 → ℕ → Std.Format

Equations

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

theorem Butcher.Z15.ext' {x y : Z15} (hr : x.re = y.re) (hi : x.im = y.im) : x = y

theorem Butcher.Z15.ext'_iff {x y : Z15} : x = y ↔ x.re = y.re ∧ x.im = y.im

@[instance_reducible]

instance Butcher.Z15.instZero : Zero Z15

Equations

• Butcher.Z15.instZero = { zero := { re := 0, im := 0 } }

@[instance_reducible]

instance Butcher.Z15.instOne : One Z15

Equations

• Butcher.Z15.instOne = { one := { re := 1, im := 0 } }

@[instance_reducible]

instance Butcher.Z15.instAdd : Add Z15

Equations

• Butcher.Z15.instAdd = { add := fun (x y : Butcher.Z15) => { re := x.re + y.re, im := x.im + y.im } }

@[instance_reducible]

instance Butcher.Z15.instNeg : Neg Z15

Equations

• Butcher.Z15.instNeg = { neg := fun (x : Butcher.Z15) => { re := -x.re, im := -x.im } }

@[instance_reducible]

instance Butcher.Z15.instSub : Sub Z15

Equations

• Butcher.Z15.instSub = { sub := fun (x y : Butcher.Z15) => { re := x.re - y.re, im := x.im - y.im } }

@[instance_reducible]

instance Butcher.Z15.instMul : Mul Z15

Equations

• Butcher.Z15.instMul = { mul := fun (x y : Butcher.Z15) => { re := x.re * y.re + 15 * x.im * y.im, im := x.re * y.im + x.im * y.re } }

@[simp]

theorem Butcher.Z15.zero_re : re 0 = 0

@[simp]

theorem Butcher.Z15.zero_im : im 0 = 0

@[simp]

theorem Butcher.Z15.one_re : re 1 = 1

@[simp]

theorem Butcher.Z15.one_im : im 1 = 0

@[simp]

theorem Butcher.Z15.add_re (x y : Z15) : (x + y).re = x.re + y.re

@[simp]

theorem Butcher.Z15.add_im (x y : Z15) : (x + y).im = x.im + y.im

@[simp]

theorem Butcher.Z15.neg_re (x : Z15) : (-x).re = -x.re

@[simp]

theorem Butcher.Z15.neg_im (x : Z15) : (-x).im = -x.im

@[simp]

theorem Butcher.Z15.sub_re (x y : Z15) : (x - y).re = x.re - y.re

@[simp]

theorem Butcher.Z15.sub_im (x y : Z15) : (x - y).im = x.im - y.im

@[simp]

theorem Butcher.Z15.mul_re (x y : Z15) : (x * y).re = x.re * y.re + 15 * x.im * y.im

@[simp]

theorem Butcher.Z15.mul_im (x y : Z15) : (x * y).im = x.re * y.im + x.im * y.re

@[instance_reducible]

instance Butcher.Z15.instCommRing : CommRing Z15

Equations

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

inductive Butcher.RTree : Type

• node : List RTree → RTree

partial def Butcher.instReprRTree.repr : RTree → ℕ → Std.Format

@[instance_reducible]

instance Butcher.instReprRTree : Repr RTree

Equations

• Butcher.instReprRTree = { reprPrec := Butcher.instReprRTree.repr }

@[instance_reducible]

instance Butcher.instInhabitedRTree : Inhabited RTree

Equations

• Butcher.instInhabitedRTree = { default := Butcher.instInhabitedRTree.default }

@[reducible, inline]

abbrev Butcher.Forest : Type

Equations

• Butcher.Forest = List Butcher.RTree

def Butcher.leaf : RTree

Equations

• Butcher.leaf = Butcher.RTree.node []

def Butcher.graft (F : Forest) : RTree

Equations

• Butcher.graft F = Butcher.RTree.node F

order and density (γ)

def Butcher.order : RTree → ℕ

Equations

• Butcher.order (Butcher.RTree.node F) = 1 + Butcher.orderF F

def Butcher.orderF : Forest → ℕ

Equations

• Butcher.orderF [] = 0
• Butcher.orderF (t :: ts) = Butcher.order t + Butcher.orderF ts

def Butcher.gamma : RTree → ℕ

density γ(t) = |t| · ∏_children γ. γ(•)=1, γ(•–•)=2, γ(cherry)=3, γ(ladder₃)=6.

Equations

• Butcher.gamma (Butcher.RTree.node F) = Butcher.order (Butcher.RTree.node F) * Butcher.gammaF F

def Butcher.gammaF : Forest → ℕ

Equations

• Butcher.gammaF [] = 1
• Butcher.gammaF (t :: ts) = Butcher.gamma t * Butcher.gammaF ts

the Butcher elementary weight Φ(t)(A,b)

A method is a tableau: `A` the stage matrix (rows), `b` the weights; #stages s = A.length.
Internal weight vector  g(t)ᵢ = ∏_children (A·g(child))ᵢ ,  leaf ↦ 𝟙.
Elementary weight  Φ(t) = bᵀ g(t).  Order conditions:  Φ(t) = 1/γ(t)  for all |t| ≤ p. 

def Butcher.dot {K : Type u_1} [CommRing K] (u v : List K) : K

Equations

• Butcher.dot u v = (List.zipWith (fun (x1 x2 : K) => x1 * x2) u v).sum

def Butcher.pmul {K : Type u_1} [CommRing K] (u v : List K) : List K

Equations

• Butcher.pmul u v = List.zipWith (fun (x1 x2 : K) => x1 * x2) u v

def Butcher.mulMatVec {K : Type u_1} [CommRing K] (A : List (List K)) (v : List K) : List K

Equations

• Butcher.mulMatVec A v = List.map (fun (row : List K) => Butcher.dot row v) A

def Butcher.phiVec {K : Type u_1} [CommRing K] (A : List (List K)) : RTree → List K

Equations

• Butcher.phiVec A (Butcher.RTree.node F) = Butcher.phiForest A F

def Butcher.phiForest {K : Type u_1} [CommRing K] (A : List (List K)) : Forest → List K

∏ over children of (A · phiVec child), pointwise; empty forest ↦ all-ones (length s).

Equations

• Butcher.phiForest A [] = List.map (fun (x : List K) => 1) A
• Butcher.phiForest A (t :: ts) = Butcher.pmul (Butcher.mulMatVec A (Butcher.phiVec A t)) (Butcher.phiForest A ts)

def Butcher.Phi {K : Type u_1} [CommRing K] (A : List (List K)) (b : List K) (t : RTree) : K

elementary weight Φ(t) = bᵀ·g(t).

Equations

• Butcher.Phi A b t = Butcher.dot b (Butcher.phiVec A t)

@[reducible, inline]

abbrev Butcher.orderCond {K : Type u_1} [CommRing K] (A : List (List K)) (b : List K) (t : RTree) : Prop

the order condition at a single tree, in MULTIPLICATIVE form γ(t)·Φ(t) = 1 (⟺ Φ(t)=1/γ(t) since γ(t) ≥ 1); stated this way it needs only a commutative ring, no division.

Equations

• Butcher.orderCond A b t = (↑(Butcher.gamma t) * Butcher.Phi A b t = 1)

the classical methods (exact rationals)

def Butcher.t1 : RTree

Equations

• Butcher.t1 = Butcher.leaf

def Butcher.t2 : RTree

Equations

• Butcher.t2 = Butcher.RTree.node [Butcher.leaf]

def Butcher.t31 : RTree

Equations

• Butcher.t31 = Butcher.RTree.node [Butcher.leaf, Butcher.leaf]

def Butcher.t32 : RTree

Equations

• Butcher.t32 = Butcher.RTree.node [Butcher.RTree.node [Butcher.leaf]]

def Butcher.t41 : RTree

Equations

• Butcher.t41 = Butcher.RTree.node [Butcher.leaf, Butcher.leaf, Butcher.leaf]

def Butcher.t42 : RTree

Equations

• Butcher.t42 = Butcher.RTree.node [Butcher.leaf, Butcher.RTree.node [Butcher.leaf]]

def Butcher.t43 : RTree

Equations

• Butcher.t43 = Butcher.RTree.node [Butcher.RTree.node [Butcher.leaf, Butcher.leaf]]

def Butcher.t44 : RTree

Equations

• Butcher.t44 = Butcher.RTree.node [Butcher.RTree.node [Butcher.RTree.node [Butcher.leaf]]]

def Butcher.t5bushy : RTree

Equations

• Butcher.t5bushy = Butcher.RTree.node [Butcher.leaf, Butcher.leaf, Butcher.leaf, Butcher.leaf]

def Butcher.euler_A : List (List ℚ)

Equations

• Butcher.euler_A = [[0]]

def Butcher.euler_b : List ℚ

Equations

• Butcher.euler_b = [1]

def Butcher.heun_A : List (List ℚ)

Equations

• Butcher.heun_A = [[0, 0], [1, 0]]

def Butcher.heun_b : List ℚ

Equations

• Butcher.heun_b = [1 / 2, 1 / 2]

def Butcher.rk4_A : List (List ℚ)

Equations

• Butcher.rk4_A = [[0, 0, 0, 0], [1 / 2, 0, 0, 0], [0, 1 / 2, 0, 0], [0, 0, 1, 0]]

def Butcher.rk4_b : List ℚ

Equations

• Butcher.rk4_b = [1 / 6, 1 / 3, 1 / 3, 1 / 6]

def Butcher.dp_A : List (List ℚ)

Equations

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

def Butcher.dp_b : List ℚ

Equations

• Butcher.dp_b = [35 / 384, 0, 500 / 1113, 125 / 192, -2187 / 6784, 11 / 84, 0]

def Butcher.gauss_A : List (List Q15)

Equations

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

def Butcher.gauss_b : List Q15

Equations

• Butcher.gauss_b = [{ re := 5 / 18, im := 0 }, { re := 4 / 9, im := 0 }, { re := 5 / 18, im := 0 }]

def Butcher.tacticGauss_check : Lean.ParserDescr

discharge a Q15 order condition: unfold the engine + cast, split into ℚ components, norm_num.

Equations

• Butcher.tacticGauss_check = Lean.ParserDescr.node `Butcher.tacticGauss_check 1024 (Lean.ParserDescr.nonReservedSymbol "gauss_check" false)

certificates — the order conditions, machine-checked (axiom-free)

Each `orderCond` unfolds the computable engine on the concrete tree/tableau to a closed ℚ
arithmetic goal, closed by `norm_num` (symbolic — sidesteps the kernel's stuck `Nat.gcd`
reduction in `Rat` normalization that defeats `decide`). 

def Butcher.tacticButcher_check : Lean.ParserDescr

unfold the engine on a concrete instance to a closed ℚ goal, then norm_num.

Equations

• Butcher.tacticButcher_check = Lean.ParserDescr.node `Butcher.tacticButcher_check 1024 (Lean.ParserDescr.nonReservedSymbol "butcher_check" false)

theorem Butcher.euler_ord1 : orderCond euler_A euler_b t1

theorem Butcher.heun_ord1 : orderCond heun_A heun_b t1

theorem Butcher.heun_ord2 : orderCond heun_A heun_b t2

theorem Butcher.heun_not_ord3 : ¬orderCond heun_A heun_b t31

theorem Butcher.rk4_ord1 : orderCond rk4_A rk4_b t1

theorem Butcher.rk4_ord2 : orderCond rk4_A rk4_b t2

theorem Butcher.rk4_ord3a : orderCond rk4_A rk4_b t31

theorem Butcher.rk4_ord3b : orderCond rk4_A rk4_b t32

theorem Butcher.rk4_ord4a : orderCond rk4_A rk4_b t41

theorem Butcher.rk4_ord4b : orderCond rk4_A rk4_b t42

theorem Butcher.rk4_ord4c : orderCond rk4_A rk4_b t43

theorem Butcher.rk4_ord4d : orderCond rk4_A rk4_b t44

theorem Butcher.rk4_not_ord5 : ¬orderCond rk4_A rk4_b t5bushy

Completeness: "order p" is exactly a finite check (order-budget generator)

A method satisfies the order-p conditions iff Φ(t)=1/γ(t) for the FINITE catalogue of trees
with |t| ≤ p.  This turns the infinite quantifier (∀ rooted trees) into a decidable
finite enumeration.  The generator `build` is bounded by an ORDER BUDGET (not by length), so the
catalogue stays Catalan-small (|trees of order ≤ p| = 1,2,4,9,23,…) and `fin_cases` is feasible
up to order 5+ (Dormand–Prince).  Structural on the budget → reduces in the kernel; completeness
is mutual induction with measure (budget, structure). 

theorem Butcher.one_le_order (t : RTree) : 1 ≤ order t

theorem Butcher.order_le_orderF_of_mem {c : RTree} {F : Forest} : c ∈ F → order c ≤ orderF F

def Butcher.build : ℕ → List RTree × List Forest

ORDER-BUDGET generator (structural on the budget n; no length over-generation). (build n).1 = all trees of order ≤ n; (build n).2 = all forests of orderF ≤ n. The filter bounds each forest by the remaining budget, keeping intermediate lists Catalan-small.

Equations

• One or more equations did not get rendered due to their size.
• Butcher.build 0 = ([], [[]])

def Butcher.treesB (n : ℕ) : List RTree

Equations

• Butcher.treesB n = (Butcher.build n).1

theorem Butcher.mem_build_trees (n : ℕ) (t : RTree) : order t ≤ n → t ∈ (build n).1

theorem Butcher.mem_build_forests (n : ℕ) (F : Forest) : orderF F ≤ n → F ∈ (build n).2

def Butcher.catalog (p : ℕ) : List RTree

the finite catalogue of all rooted trees with |t| ≤ p.

Equations

• Butcher.catalog p = List.filter (fun (t : Butcher.RTree) => decide (Butcher.order t ≤ p)) (Butcher.treesB p)

def Butcher.satisfiesOrderConditions {K : Type u_1} [CommRing K] (A : List (List K)) (b : List K) (p : ℕ) : Prop

a method (A,b) satisfies the order-p conditions: every order condition holds through order p.

Equations

• Butcher.satisfiesOrderConditions A b p = ∀ (t : Butcher.RTree), Butcher.order t ≤ p → Butcher.orderCond A b t

theorem Butcher.satisfiesOrderConditions_iff {K : Type u_1} [CommRing K] (A : List (List K)) (b : List K) (p : ℕ) : satisfiesOrderConditions A b p ↔ ∀ t ∈ catalog p, orderCond A b t

The order-p conditions ⟺ a finite check over the catalogue (sound and complete).

theorem Butcher.rk4_order4 : satisfiesOrderConditions rk4_A rk4_b 4

classic RK4 satisfies ALL order-≤4 conditions, certified, axiom-free.

The planar → abstract bridge: Φ is symmetric in a node's children

Our trees are PLANAR (ordered children).  The numerical literature uses ABSTRACT rooted trees
(multiset children); the abstract Connes–Kreimer algebra is the abelianization (Foissy 2002) of
our noncommutative one.  Here we prove the order condition descends along that symmetrization:
permuting the children of a node leaves Φ, γ and hence the order condition unchanged.  So
certifying all PLANAR trees of order ≤ p genuinely subsumes the abstract order conditions —
mirror planar trees (same abstract shape) share a single condition.  Engine of the bridge:
`pmul` (pointwise ℚ-product of stage vectors) is commutative and associative UNconditionally. 

theorem Butcher.pmul_comm (u v : List ℚ) : pmul u v = pmul v u

theorem Butcher.pmul_assoc (u v w : List ℚ) : pmul (pmul u v) w = pmul u (pmul v w)

theorem Butcher.phiForest_perm (A : List (List ℚ)) {F G : Forest} (h : List.Perm F G) : phiForest A F = phiForest A G

theorem Butcher.orderF_perm {F G : Forest} (h : List.Perm F G) : orderF F = orderF G

theorem Butcher.gammaF_perm {F G : Forest} (h : List.Perm F G) : gammaF F = gammaF G

theorem Butcher.Phi_node_perm (A : List (List ℚ)) (b : List ℚ) {F G : Forest} (h : List.Perm F G) : Phi A b (RTree.node F) = Phi A b (RTree.node G)

Φ is invariant under permuting the children of the root.

theorem Butcher.gamma_node_perm {F G : Forest} (h : List.Perm F G) : gamma (RTree.node F) = gamma (RTree.node G)

γ is invariant under permuting the children of the root.

theorem Butcher.orderCond_node_perm (A : List (List ℚ)) (b : List ℚ) {F G : Forest} (h : List.Perm F G) : orderCond A b (RTree.node F) ↔ orderCond A b (RTree.node G)

The order condition depends only on the abstract tree: permuting children is invisible.

A higher-order method: Dormand–Prince certified order 5

The order-budget generator makes `catalog 5` (23 planar trees) small enough that `fin_cases`
discharges every order-≤5 condition for the 7-stage DOPRI5 tableau (the default method of
MATLAB `ode45` and SciPy `RK45`).  (Heartbeat bump: `fin_cases` whnf-reduces the 23-tree catalogue — a
finite computation, just slow in the elaborator; no effect on the axiom set.) 

theorem Butcher.dp_order5 : satisfiesOrderConditions dp_A dp_b 5

An implicit method with algebraic coefficients: Gauss–Legendre s=3

Gauss–Legendre with 3 stages is fully implicit, with a tableau living in ℚ(√15).  Working in the
computable pair ring `Q15` (where √15²=15 is baked into multiplication), every order condition
collapses to a pair of ℚ identities that `gauss_check` closes by `norm_num` — no algebraic-number
tactic.  This certifies the framework on implicit methods with irrational (algebraic) coefficients.

We certify order 4 here by this route; by `fin_cases` over `catalog 6` (65 planar trees) with
`norm_num` it does not complete in practical time. Order 6 is certified below over the integers. 

theorem Butcher.gauss_order4 : satisfiesOrderConditions gauss_A gauss_b 4

Gauss–Legendre s=3 to order 6 (integer ℤ[√15] + decide)

`gauss_order4` above unfolds the engine symbolically and closes the ℚ(√15) components by `norm_num`.
At order 6 that route dies: the 65 per-tree `norm_num` calls exhaust memory,
because ℚ's `Nat.gcd` normalization does not reduce in the kernel and the unfolded Q15 products are
huge.  The fix is to clear all denominators.  Scaling the tableau by `D = 360` (the lcm of the denominators
36,9,15,30,24,18) lands it in the INTEGER ring `Z15 = ℤ[√15]`.  The elementary weight is homogeneous,
`Φ(D·A, D·b, t) = D^{|t|}·Φ(A,b,t)`, so the order condition `γ(t)·Φ = 1` becomes the integer identity
`γ(t)·Φ(D·A,D·b,t) = D^{|t|}`.  Over `Z15` (a pair of `Int`) this closes by `decide`: the kernel's
GMP `Int` arithmetic evaluates it directly — no rational normalization, negligible memory.  The whole
certificate (all 65 planar trees of `catalog 6`) checks in about a second.

Not formalized here: the homogeneity of `Φ`, and that `gaussI_A`, `gaussI_b` are `D` times
`gauss_A`, `gauss_b` entrywise; together they make the integer conditions equivalent to the
unscaled ones. `gauss_order6` is the statement about the scaled integer tableau.

The scaled integer tableau: entry `a + b√15` with denominator cleared by 360 becomes `⟨360a, 360b⟩`.
E.g. `2/9 - √15/15 ↦ ⟨80, -24⟩`, `5/18 ↦ ⟨100,0⟩`. 

def Butcher.gaussI_A : List (List Z15)

Equations

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

def Butcher.gaussI_b : List Z15

Equations

• Butcher.gaussI_b = [{ re := 100, im := 0 }, { re := 160, im := 0 }, { re := 100, im := 0 }]

def Butcher.Dscale : ℤ

Equations

• Butcher.Dscale = 360

@[reducible, inline]

abbrev Butcher.orderCondInt (A : List (List Z15)) (b : List Z15) (D : ℤ) (t : RTree) : Prop

the order condition with denominators cleared: γ(t)·Φ(D·A,D·b,t) = D^{|t|} in Z15. Equivalent to orderCond on the unscaled ℚ(√15) tableau by homogeneity of Φ, but decidable by the kernel.

Equations

• Butcher.orderCondInt A b D t = ({ re := ↑(Butcher.gamma t), im := 0 } * Butcher.Phi A b t = { re := D ^ Butcher.order t, im := 0 })

def Butcher.satisfiesOrderConditionsInt (A : List (List Z15)) (b : List Z15) (D : ℤ) (p : ℕ) : Prop

Equations

• Butcher.satisfiesOrderConditionsInt A b D p = ∀ (t : Butcher.RTree), Butcher.order t ≤ p → Butcher.orderCondInt A b D t

theorem Butcher.satisfiesOrderConditionsInt_iff (A : List (List Z15)) (b : List Z15) (D : ℤ) (p : ℕ) : satisfiesOrderConditionsInt A b D p ↔ ∀ t ∈ catalog p, orderCondInt A b D t

Same reduction as satisfiesOrderConditions_iff, for the integer condition: the order-p conditions reduce to the finite catalogue check (reuses the generic build/catalog completeness).

Gauss–Legendre s=3 satisfies ALL order-≤6 conditions: the full order-6 certificate, axiom-free. fin_cases enumerates the 65-tree catalogue; each condition is closed by the kernel (decide) over Z15 integer arithmetic. (Heartbeat bump bounds only fin_cases' elaboration; the per-tree decide is cheap and has no effect on the axiom set.)

theorem Butcher.gauss_order6 : satisfiesOrderConditionsInt gaussI_A gaussI_b Dscale 6

Examples

Orders and densities of the small trees, and the sizes of the catalogues: the numbers of planar rooted trees with at most p nodes (1, 2, 4, 9, 23, partial sums of Catalan numbers), not of abstract rooted trees.