LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Quadratic interpolation gives the variable-step BDF2 formula and cubic residual

Statement

Let $h_{n - 1}, h_{n} > 0$ , $r_{n} = h_{n} / h_{n - 1}$ , and let $y$ be an exact solution with three continuous derivatives near $t_{n - 1}, t_{n}, t_{n + 1}$ , where $h_{j} = t_{j + 1} - t_{j}$ . The derivative at $t_{n + 1}$ of the quadratic interpolant through $(t_{n + 1}, y_{n + 1})$ , $(t_{n}, y_{n})$ , and $(t_{n - 1}, y_{n - 1})$ is

$\frac{(1 + 2 r_{n}) y_{n + 1} - (1 + r_{n})^{2} y_{n} + r_{n}^{2} y_{n - 1}}{h_{n} (1 + r_{n})} .$

Equating this derivative to $f (t_{n + 1}, Y_{n + 1})$ defines the variable-step BDF2 formula

$\frac{(1 + 2 r_{n}) Y_{n + 1} - (1 + r_{n})^{2} Y_{n} + r_{n}^{2} Y_{n - 1}}{h_{n} (1 + r_{n})} = f (t_{n + 1}, Y_{n + 1}) .$

For an exact vector solution $y^{'} = f (t, y)$ whose third derivative is bounded, the unscaled residual

$τ_{n} = (1 + 2 r_{n}) y (t_{n + 1}) - (1 + r_{n})^{2} y (t_{n}) + r_{n}^{2} y (t_{n - 1}) - h_{n} (1 + r_{n}) y^{'} (t_{n + 1})$

has norm $∥ τ_{n} ∥_{\infty} = O (h_{n}^{3})$ uniformly whenever $r_{n}$ stays in a fixed compact subinterval of $(0, \infty)$ ; the formula and remainder hold componentwise.

Facts & Assumptions

Given: Distinct ordered nodes $t_{n - 1} < t_{n} < t_{n + 1}$ , their positive step sizes, and the linear multistep coefficient convention in Linear multistep methods, consistency, order, and the root condition.

[F1]

Multivariable Taylor formula with a Lagrange remainder along a line segment applies separately to every real coordinate of $y$ on the interval between the nodes. For a component with $∣ y_{i}^{(3)} ∣ \leq M$ , its degree-two remainder at displacement $δ$ has absolute value at most $M ∣ δ ∣^{3} / 6$ ; the intermediate points may differ by component and node. Taking the maximum of these finitely many component bounds gives the same max-norm estimate, without a common vector remainder point.

Proof

1.1givenconstructalgebra

Set $s = (t - t_{n + 1}) / h_{n}$ . The interpolation nodes become $0, - 1, - (1 + 1 / r_{n})$ . Their Lagrange basis derivatives at $s = 0$ are respectively $(1 + 2 r_{n}) / (1 + r_{n})$ , $- (1 + r_{n})$ , and $r_{n}^{2} / (1 + r_{n})$ , as follows by differentiating the three quadratic basis products. Since $d s / d t = 1 / h_{n}$ , the derivative formula in the statement follows.

1.2F1algebra

Apply [F1] separately to each component at $t_{n + 1}$ through degree two. In the weighted combination $S = (1 + 2 r_{n}) y (t_{n + 1}) - (1 + r_{n})^{2} y (t_{n}) + r_{n}^{2} y (t_{n - 1})$ , the constant coefficient is zero; the coefficient of $y^{'}$ is $(1 + r_{n}) h_{n}$ ; and the coefficient of $y^{''}$ is $- \frac{1}{2} (1 + r_{n})^{2} h_{n}^{2} + \frac{1}{2} r_{n}^{2} (h_{n} + h_{n - 1})^{2} = 0$ .

2.1F1step 1.2algebra∎

Let $M$ bound the absolute third derivatives of every component. By [F1], the max norm of the remaining weighted remainders is at most $(M / 6) ((1 + r_{n})^{2} h_{n}^{3} + r_{n}^{2} (h_{n} + h_{n - 1})^{3})$ . On the fixed compact ratio interval, $h_{n - 1} = h_{n} / r_{n}$ makes this at most $C h_{n}^{3}$ with a uniform finite $C$ . The canceled terms in step 1.2 leave exactly these remainders after subtracting the exact derivative term, so $∥ τ_{n} ∥_{\infty} \leq C h_{n}^{3}$ .

Depends on

Used by

Dependency tree · two levels

12 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, Syvert P. Nørsett, and Gerhard Wanner, Solving Ordinary Differential Equations I: Nonstiff Problems, 2nd ed., Chapter III.5, pp. 397–401 (standard reference, not scraped)
G. Söderlind, L. Wang, and S. Zhang, On the zero-stability of multistep methods on smooth nonuniform grids, §4 (standard reference, not scraped)