Gauss–Legendre with three stages does not have order 7

The three-stage Gauss–Legendre method has order 6 (Butcher.gauss_order6) and not order 7. The witness is the bushy tree with seven nodes (root with six leaves), whose order condition is the quadrature condition ∑ bᵢ cᵢ⁶ = 1/7; a three-node Gauss rule is exact only up to degree 5.

Main results

• Butcher.gauss_not_ord7: the unscaled ℚ(√15) tableau fails the order condition on the bushy tree with seven nodes.
• Butcher.gauss_not_order7: hence ¬ satisfiesOrderConditions gauss_A gauss_b 7.
• Butcher.gaussI_not_ord7, Butcher.gaussI_exact_order6: the same failure for the scaled integer tableau of Butcher.gauss_order6, and with it "order 6 and not 7" for that tableau.
• Butcher.gaussI_all_ord7_fail: every planar tree with exactly seven nodes fails the scaled integer condition (132 planar trees; the paper counts the 48 abstract ones).

References

• E. Hairer, C. Lubich, G. Wanner, Geometric Numerical Integration, Springer (2006).
• 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, Section 6.

def Butcher.t7bushy : RTree

The bushy tree with seven nodes: a root with six leaves. γ = 7.

Equations

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

theorem Butcher.gauss_not_ord7 : ¬orderCond gauss_A gauss_b t7bushy

Gauss–Legendre s = 3 fails the order condition on the bushy seven-node tree.

theorem Butcher.gauss_not_order7 : ¬satisfiesOrderConditions gauss_A gauss_b 7

Gauss–Legendre s = 3 does not satisfy the order conditions of order 7.

theorem Butcher.gaussI_not_ord7 : ¬orderCondInt gaussI_A gaussI_b Dscale t7bushy

The scaled integer tableau fails the cleared order condition on the bushy seven-node tree.

theorem Butcher.gaussI_exact_order6 : satisfiesOrderConditionsInt gaussI_A gaussI_b Dscale 6 ∧ ¬satisfiesOrderConditionsInt gaussI_A gaussI_b Dscale 7

The scaled integer Gauss–Legendre tableau satisfies the cleared conditions through order 6 and not through order 7.

theorem Butcher.gaussI_all_ord7_fail (t : RTree) : t ∈ catalog 7 → order t = 7 → ¬orderCondInt gaussI_A gaussI_b Dscale t

Every planar tree with exactly seven nodes fails the cleared order condition.