LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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 variable-step BDF2 parasitic increment contracts below the sharp ratio threshold

Statement

For the homogeneous vector-valued variable-step BDF2 recurrence obtained from Variable-step BDF2 with an explicit local implicit-branch rule by setting $f = 0$ , let $Δ_{n} = Y_{n} - Y_{n - 1} \in R^{d}$ . For every $r_{n} = h_{n} / h_{n - 1} > 0$ ,

$Δ_{n + 1} = q (r_{n}) Δ_{n}, q (r) = \frac{r^{2}}{1 + 2 r} .$

The multiplier satisfies $q (r) \leq 1$ exactly when $0 < r \leq 1 + \sqrt{2}$ . In particular, if $0 < r_{n} \leq r_{*} < 1 + \sqrt{2}$ for every step, then $q (r_{n}) \leq q_{*} : = r_{*}^{2} / (1 + 2 r_{*}) < 1$ uniformly.

Facts & Assumptions

Given: The homogeneous variable-step BDF2 equation and the positive step-ratio convention in Variable-step BDF2 with an explicit local implicit-branch rule.

[L1]

Quadratic interpolation gives the variable-step BDF2 formula and cubic residual gives the BDF2 coefficients $(1 + 2 r_{n}), - (1 + r_{n})^{2}, r_{n}^{2}$ .

Proof

1.1givenL1algebra

With $f = 0$ , the recurrence is $(1 + 2 r_{n}) Y_{n + 1} - (1 + r_{n})^{2} Y_{n} + r_{n}^{2} Y_{n - 1} = 0$ . Substitute $Y_{n + 1} = Y_{n} + Δ_{n + 1}$ and $Y_{n - 1} = Y_{n} - Δ_{n}$ ; the coefficient of $Y_{n}$ cancels, leaving $(1 + 2 r_{n}) Δ_{n + 1} = r_{n}^{2} Δ_{n}$ .

2.1step 1.1algebra

Since $1 + 2 r_{n} > 0$ , division gives $Δ_{n + 1} = q (r_{n}) Δ_{n}$ . The derivative $q^{'} (r) = 2 r (1 + r) / (1 + 2 r)^{2}$ is positive for $r > 0$ , while $q (r) \leq 1$ is equivalent to $r^{2} - 2 r - 1 \leq 0$ , or $r \leq 1 + \sqrt{2}$ .

3.1step 2.1algebra∎

The function $q$ is continuous and increasing, so for $r_{n} \leq r_{*} < 1 + \sqrt{2}$ its maximum is $q_{*} < 1$ . This proves the uniform contraction claim.

Depends on

Used by

Dependency tree · two levels

5 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

G. Söderlind, L. Wang, and S. Zhang, On the zero-stability of multistep methods on smooth nonuniform grids, §4 (standard reference, not scraped)
Ernst Hairer, Syvert P. Nørsett, and Gerhard Wanner, Solving Ordinary Differential Equations I: Nonstiff Problems, 2nd ed., Chapter III.5, Stability, pp. 402–406 (standard reference, not scraped)