Certified Runge-Kutta Order Conditions #
This file checks concrete Runge-Kutta methods against their rooted-tree Butcher
order conditions. It defines a small computable engine for planar rooted trees,
the density γ, and the elementary weight Φ(A,b), proves the finite-catalogue
keystone for order conditions, and verifies Euler, Heun, RK4, Dormand-Prince,
and Gauss-Legendre certificates.
ℚ(√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
(order 6) tableau (Brick 5). Working in this concrete pair ring keeps the
order-condition checks a pure ℚ component computation closed by norm_num — no
algebraic-number tactic needed.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
ℤ[√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 Brick 6 to certify Gauss order 6 by decide after the
tableau is cleared of denominators (scaled by D=360).
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
An ordered forest of planar rooted trees.
Instances For
The one-node rooted tree.
Instances For
Graft a forest below a new root.
Instances For
order and density (γ) #
Number of vertices in a rooted tree.
Equations
Instances For
Total number of vertices in a forest.
Equations
Instances For
density γ(t) = |t| · ∏_children γ. γ(•)=1, γ(•–•)=2, γ(cherry)=3, γ(ladder₃)=6.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Product of the densities of the trees in a forest.
Equations
Instances For
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.
Dot product of two coefficient vectors, truncated to the shorter length.
Equations
- RungeKuttaOrderConditions.Butcher.dot u v = (List.zipWith (fun (x1 x2 : K) => x1 * x2) u v).sum
Instances For
Pointwise product of two coefficient vectors, truncated to the shorter length.
Equations
- RungeKuttaOrderConditions.Butcher.pmul u v = List.zipWith (fun (x1 x2 : K) => x1 * x2) u v
Instances For
Matrix-vector product for a list-of-rows matrix.
Equations
- RungeKuttaOrderConditions.Butcher.mulMatVec A v = List.map (fun (row : List K) => RungeKuttaOrderConditions.Butcher.dot row v) A
Instances For
Internal elementary weight vector for a rooted tree.
Equations
Instances For
∏ over children of (A · phiVec child), pointwise; empty forest ↦ all-ones (length s).
Equations
Instances For
the order condition at a single tree, in MULTIPLICATIVE form γ(t)·Φ(t) = 1
(iff Φ(t)=1/γ(t) since γ(t) ≥ 1); stated this way it needs only a commutative
ring, no division.
Equations
Instances For
the classical methods (exact rationals) #
The unique tree of order 1.
Instances For
The ladder tree of order 2.
Equations
Instances For
The two-leaf cherry tree of order 3.
Equations
Instances For
The ladder tree of order 3.
Equations
Instances For
The four-vertex bushy tree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A mixed order-4 tree with one leaf and one order-2 child.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The order-4 tree with a cherry child.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ladder tree of order 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The five-vertex bushy tree used to witness RK4's order-5 failure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Weights for the Euler method.
Equations
Instances For
Weights for Heun's explicit trapezoid method.
Equations
- RungeKuttaOrderConditions.Butcher.heunB = [1 / 2, 1 / 2]
Instances For
Stage matrix for the Dormand-Prince RK45 method.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stage matrix for the three-stage Gauss-Legendre method over ℚ(√15).
Equations
- One or more equations did not get rendered due to their size.
Instances For
discharge a Q15 order condition: unfold the engine + cast, split into ℚ components,
norm_num.
Equations
- RungeKuttaOrderConditions.Butcher.tacticGaussCheck = Lean.ParserDescr.node `RungeKuttaOrderConditions.Butcher.tacticGaussCheck 1024 (Lean.ParserDescr.nonReservedSymbol "gaussCheck" false)
Instances For
Cross-checks against Sage/bseries.py ground truth #
The sample orders are 1, 2, 3, 3, 4, 4, 5, the sample tree factorials are
1, 2, 3, 6, 4, 8, 12, 24, 5, and the RK4 elementary weights match 1 / γ
through order 4 but give 5 / 24 on t5bushy where 1 / γ = 1 / 5.
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`).
unfold the engine on a concrete instance to a closed ℚ goal, then norm_num.
Equations
- RungeKuttaOrderConditions.Butcher.tacticButcherCheck = Lean.ParserDescr.node `RungeKuttaOrderConditions.Butcher.tacticButcherCheck 1024 (Lean.ParserDescr.nonReservedSymbol "butcherCheck" false)
Instances For
Brick 2+4 — 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. Keystone: it 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) — the "WF wall" was imaginary (Socratic).
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
Instances For
Trees generated by the order-budget catalogue up to order n.
Instances For
the finite catalogue of all rooted trees with |t| ≤ p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
a method (A,b) satisfies the order-p conditions: every order condition holds through
order p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
classic RK4 satisfies ALL order-≤4 conditions, certified, axiom-free.
Brick 3 — 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.
γ is invariant under permuting the children of the root.
Brick 4 — 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. First machine-checked
certificate that a production RK method (the default in MATLAB `ode45`, SciPy `RK45`) attains
its full classical order.
Brick 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
`gaussCheck` 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 direct symbolic route. At order 6 the same
route dies: a `fin_cases` over `catalog 6` (65 planar trees) with per-tree
`norm_num` is dominated by the elaborator's whnf reduction of the catalogue
and does not complete in practical time at this scale. The full order-6
certificate `satisfiesOrderConditions gaussA gaussB 6` is instead
`gauss_order6_rat` below: Brick 6 clears denominators into ℤ[√15] and
certifies the scaled tableau by `decide`, and Brick 7 transports the result
back to `gaussA`/`gaussB` through the formalized homogeneity bridge.
Brick 6 — Gauss–Legendre s=3 certified to FULL 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 (a run reached ~20 GB), because ℚ's `Nat.gcd` normalization
does not reduce in the kernel and the unfolded Q15 products are huge. The fix is
a genuinely different *formula* (found by re-questioning the representation, not
the method): 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 ~1 s, axiom-free. Cross-checked outside Lean three ways
(tree recursion + brute-force index sum in Python, brute-force in Sage over ℚ(√15)):
Gauss s=3 holds orders 1–6 and fails all 48 order-7 conditions, i.e. it is EXACTLY order 6.
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⟩`.
Denominator-cleared stage matrix for the three-stage Gauss-Legendre method.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common denominator used to scale the Gauss-Legendre tableau.
Equations
Instances For
the order condition with denominators cleared: γ(t)·Φ(D·A,D·b,t) = D^{|t|}
in Z15, decidable by the kernel. The equivalence with orderCond on the
unscaled ℚ(√15) tableau is the homogeneity bridge, formalized in Brick 7 and
consumed by gauss_order6_rat.
Equations
- One or more equations did not get rendered due to their size.
Instances For
same keystone 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 for the scaled tableau:
the integer certificate, axiom-free.
fin_cases enumerates the 65-tree catalogue; each condition is closed by the kernel (decide)
over Z15 integer arithmetic. Brick 7 below transports this certificate back
to the rational tableau (gauss_order6_rat).
Brick 7 — the homogeneity bridge: the order-6 certificate over ℚ(√15) #
`gauss_order6` certifies the 360-scaled tableau over `Z15`. Two generic facts
transport it back to the true rational tableau: the engine commutes with the
componentwise inclusion `Z15 → Q15` (`Phi_toQ15`), and `Φ` is homogeneous of
degree `|t|` under entrywise scaling of the tableau (`Phi_smulVec`). In `Q15`
the factor `⟨360,0⟩^{|t|}` has the explicit inverse `⟨(1/360)^{|t|},0⟩`, so the
scaled condition divides back to `orderCond gaussA gaussB t`, yielding the
real-tableau certificate `gauss_order6_rat` — pointwise, no `fin_cases`.
Entrywise scaling of a coefficient vector.
Equations
- RungeKuttaOrderConditions.Butcher.smulVec c v = List.map (fun (x : K) => c * x) v
Instances For
Entrywise scaling of a stage matrix (each row scaled entrywise).
Equations
Instances For
Gauss–Legendre s=3 satisfies ALL order-≤6 conditions over the true ℚ(√15)
tableau gaussA, gaussB: the full order-6 certificate, obtained from the
scaled integer certificate gauss_order6 through the homogeneity bridge.