ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The leading Euler–Heun estimator coefficient can vanish

Example

Apply the Euler–Heun pair to $y^{'} = t^{2}$ , $y (0) = 0$ , on one step of size $h > 0$ . The low-order defect begins at order $h^{3}$ , not $h^{2}$ , so the embedded difference is not asymptotically equal to the low-order defect in ratio.

Facts & Assumptions

Given: The field $f (t, y) = t^{2}$ , initial time and value $t_{0} = y_{0} = 0$ , and $h > 0$ .

[F1]

Euler–Heun embedded Runge–Kutta pair: $K_{1} = f (0, 0)$ , $K_{2} = f (h, h K_{1})$ , $Y_{E} = h K_{1}$ , and $Y_{H} = \frac{h}{2} (K_{1} + K_{2})$ .

[F2]

Local orders and leading estimator term for the Euler–Heun pair: the local error expansions compare each one-step value with the exact endpoint.

[F3]

A nonzero leading defect makes the embedded difference asymptotically match the low-order defect: a ratio-one conclusion requires a nonzero leading low-defect coefficient.

Verification

1.1givenF1F2algebra

Here $K_{1} = 0$ and $K_{2} = h^{2}$ , so $Y_{E} = 0$ and $Y_{H} = h^{3} / 2$ . Since $y (h) = \int_{0}^{h} t^{2} d t = h^{3} / 3$ , the Euler defect is $- h^{3} / 3$ , the Heun defect is $h^{3} / 6$ , and the embedded estimator is $∣ Y_{H} - Y_{E} ∣ = h^{3} / 2$ .

2.1F1F3step 1.1algebra∎

The Euler defect has zero coefficient at order $h^{2}$ and the estimator-to-Euler-defect ratio is $(h^{3} / 2) / (h^{3} / 3) = 3 / 2$ for every $h > 0$ . This concrete case shows why [F3] requires a nonzero leading coefficient before asserting ratio one.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ernst Hairer, course notes, Chapter III: Équations Différentielles Ordinaires, §III.2 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Chapter 6 (standard reference, not scraped)