TheoremStatement: 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.

Coupled constant-step BDF2 is second order for a regular index-one DAE

Statement

For the semi-explicit DAE with $x \in R^{d}$ , $z \in R^{m}$ , and $d, m \geq 1$ , let $x^{'} = F (t, x)$ be the reduced ODE from A regular index-one DAE has a local reduced ODE branch on $[0, T]$ , with exact solution $\overset{ˉ}{x} \in C^{3}$ . Assume $F$ is Lipschitz in $x$ on a common compact tube with constant $L$ , $ψ$ is Lipschitz in $x$ there with constant $L_{ψ}$ , $f$ is Lipschitz in $z$ with constant $L_{z}$ , and the residual lemma's hypotheses hold uniformly on this tube: common $γ > 0$ , $Λ \geq 0$ , and $ρ > 0$ in its lower singular-value and Jacobian-Lipschitz bounds, with $ρ \leq γ / (\sqrt{m} Λ)$ when $Λ > 0$ . Every numerical algebraic candidate lies in its corresponding branch ball. Use a constant grid $t_{n} = n h$ , $h = T / N$ , $T > 0$ , and $N \geq 2$ . Suppose the two starting pairs satisfy

∥ X_{j} - \overset{ˉ}{x} (t_{j}) ∥_{2} \leq C_{s} h^{2}, ∥ g (t_{j}, X_{j}, Z_{j}) ∥_{2} \leq C_{a, s} h^{2}, j = 0, 1.

For each $2 \leq n \leq N$ , suppose the constant-step BDF2 derivative and algebraic residuals satisfy

r_{n}^{d} = \frac{3 X_{n} - 4 X_{n - 1} + X_{n - 2}}{2 h} - f (t_{n}, X_{n}, Z_{n}), r_{n}^{a} = g (t_{n}, X_{n}, Z_{n}), ∥ r_{n}^{d} ∥_{2} \leq C_{d} h^{2}, ∥ r_{n}^{a} ∥_{2} \leq C_{a} h^{2} .

Then, for all sufficiently small $h$ , a constant $C$ independent of $h$ satisfies

\max_{0 \leq n \leq N} (∥ X_{n} - \overset{ˉ}{x} (t_{n}) ∥_{2} + ∥ Z_{n} - ψ (t_{n}, \overset{ˉ}{x} (t_{n})) ∥_{2}) \leq C h^{2} .

The starter hypothesis holds, in particular, for an exact consistent $X_{0}, Z_{0}$ and one backward-Euler startup from $X_{0}$ with derivative residual $O (h)$ and algebraic residual $O (h^{2})$ . The error theorem is conditional on the residual bounds and selected branch; it does not assert that a finite Newton budget meets them.

Facts & Assumptions

Given: A $C^{3}$ reduced solution on a compact tube, a selected $C^{2}$ index-one branch, the Lipschitz bounds, a constant grid, the starting-pair bounds, the BDF2 residuals, and the residual branch hypotheses in the Statement.

[F1]

A regular index-one DAE has a local reduced ODE branch: the reduced field is $F (t, x) = f (t, x, ψ (t, x))$ , and the DAE algebraic variable is $ψ (t, x)$ .

[F2]

An index-one algebraic residual locally bounds algebraic state error: inside its branch ball, algebraic residual $r^{a}$ gives $∥ Z - ψ (t, X) ∥_{2} \leq (2 / γ) ∥ r^{a} ∥_{2}$ .

[F3]

Finite-budget coupled constant-step BDF2 for an index-one DAE: the coupled differential residual is $r_{n}^{d} = (3 X_{n} - 4 X_{n - 1} + X_{n - 2}) / (2 h) - f (t_{n}, X_{n}, Z_{n})$ . Its coefficients are the constant-step case $r_{n} = 1$ of Variable-step BDF2 with an explicit local implicit-branch rule; on the exact selected branch, [F1] gives $f (t_{n}, X_{n}, ψ (t_{n}, X_{n})) = F (t_{n}, X_{n})$ .

[F4]

Quadratic interpolation gives the variable-step BDF2 formula and cubic residual: for $C^{3}$ exact solutions and constant adjacent-step ratio $1$ , the unscaled exact BDF2 residual is $O (h^{3})$ .

[F5]

Finite geometric error bound from a one-step recurrence: a recurrence $E_{n} \leq (1 + L_{0} h) E_{n - 1} + C_{1} h^{3}$ with $E_{1} = O (h^{2})$ on a finite uniform interval has $\max_{n} E_{n} = O (h^{2})$ .

[F6]

Multivariable Taylor formula with a Lagrange remainder along a line segment: Taylor expansion with bounded third derivative gives the stated cubic local BDF2 residual.

[A1]

All exact and numerical states, algebraic residual candidates, and selected roots lie in the common compact tube and branch balls of the Statement, with the same $γ, Λ, ρ$ at every step.

Proof

1.1A1F1F2algebra

Write ${\overset{ˉ}{x}}_{n} = \overset{ˉ}{x} (t_{n})$ , ${\overset{ˉ}{z}}_{n} = ψ (t_{n}, {\overset{ˉ}{x}}_{n})$ , and $e_{n} = X_{n} - {\overset{ˉ}{x}}_{n}$ . By [F2], $∥ Z_{n} - ψ (t_{n}, X_{n}) ∥_{2} \leq (2 C_{a} / γ) h^{2}$ . Thus, with $δ_{n} = f (t_{n}, X_{n}, Z_{n}) - F (t_{n}, X_{n})$ , the $z$ -Lipschitz bound gives $∥ δ_{n} ∥_{2} \leq (2 L_{z} C_{a} / γ) h^{2}$ .

1.2A1F4F6

Put $τ_{n} = (3 {\overset{ˉ}{x}}_{n} - 4 {\overset{ˉ}{x}}_{n - 1} + {\overset{ˉ}{x}}_{n - 2}) / (2 h) - F (t_{n}, {\overset{ˉ}{x}}_{n})$ . By [F4], setting the adjacent-step ratio to $1$ gives an unscaled residual of size $O (h^{3})$ ; division by $2 h$ yields $∥ τ_{n} ∥_{2} \leq C_{τ} h^{2}$ . This also follows by applying [F6] componentwise to the exact solution through degree two.

2.1A1F3step 1.1step 1.2algebra

By [F3] and step 1.1, the numerical recurrence is $(3 X_{n} - 4 X_{n - 1} + X_{n - 2}) / (2 h) = F (t_{n}, X_{n}) + δ_{n} + r_{n}^{d}$ , while the exact defect definition gives the same formula with $X$ replaced by $\overset{ˉ}{x}$ and an added $τ_{n}$ . With $d_{n} = e_{n} - e_{n - 1}$ and $w_{n} = δ_{n} + r_{n}^{d} - τ_{n}$ , subtraction gives $3 d_{n} - d_{n - 1} = 2 h (F (t_{n}, X_{n}) - F (t_{n}, {\overset{ˉ}{x}}_{n}) + w_{n})$ , where $∥ w_{n} ∥_{2} \leq q_{n} : = ∥ r_{n}^{d} ∥_{2} + ∥ δ_{n} ∥_{2} + ∥ τ_{n} ∥_{2}$ . The Lipschitz bound and $∥ e_{n} ∥_{2} \leq ∥ e_{n - 1} ∥_{2} + ∥ d_{n} ∥_{2}$ imply $(3 - 2 h L) ∥ d_{n} ∥_{2} \leq ∥ d_{n - 1} ∥_{2} + 2 h L ∥ e_{n - 1} ∥_{2} + 2 h q_{n}$ . For $h L \leq 3 / 4$ , division by $3 - 2 h L \geq 3 / 2$ yields $∥ d_{n} ∥_{2} \leq (2 / 3) ∥ d_{n - 1} ∥_{2} + (4 / 3) h L ∥ e_{n - 1} ∥_{2} + (4 / 3) h q_{n}$ .

3.1step 2.1step 1.1step 1.2algebra

Set $E_{n} = ∥ e_{n} ∥_{2} + 2 ∥ d_{n} ∥_{2}$ . Using $e_{n} = e_{n - 1} + d_{n}$ and the last inequality of step 2.1 gives $E_{n} \leq (1 + 4 L h) ∥ e_{n - 1} ∥_{2} + 2 ∥ d_{n - 1} ∥_{2} + 4 h q_{n} \leq (1 + 4 L h) E_{n - 1} + 4 h q_{n}$ . Steps 1.1 and 1.2 and the residual assumptions imply $q_{n} \leq C_{q} h^{2}$ , so $E_{n} \leq (1 + 4 L h) E_{n - 1} + 4 C_{q} h^{3}$ .

4.1F5step 3.1given

The starting-pair bounds give $E_{1} \leq ∥ e_{1} ∥_{2} + 2 ∥ e_{1} - e_{0} ∥_{2} = O (h^{2})$ . Apply [F5] to the $N - 1$ steps from index $1$ to $N$ , whose interval length is $(N - 1) h \leq T$ . This yields $\max_{1 \leq n \leq N} E_{n} = O (h^{2})$ ; the starting-pair bound also gives $∥ e_{0} ∥_{2} = O (h^{2})$ , so $\max_{0 \leq n \leq N} ∥ e_{n} ∥_{2} = O (h^{2})$ .

5.1A1F1F2step 4.1algebra

The residual estimate [F2] and the Lipschitz bound on $ψ$ give $∥ Z_{n} - {\overset{ˉ}{z}}_{n} ∥_{2} \leq ∥ Z_{n} - ψ (t_{n}, X_{n}) ∥_{2} + L_{ψ} ∥ e_{n} ∥_{2} = O (h^{2})$ for every $n$ , including $n = 0, 1$ by the starter assumptions.

6.1A1F1F2F6algebra∎

To verify the stated backward-Euler startup option, let $X_{0} = {\overset{ˉ}{x}}_{0}$ . Its exact-start BE defect satisfies $τ_{1}^{B E} = ({\overset{ˉ}{x}}_{1} - {\overset{ˉ}{x}}_{0}) / h - F (t_{1}, {\overset{ˉ}{x}}_{1}) = O (h)$ by [F6]. The BE residual equation and Lipschitz bound then give $(1 - h L) ∥ X_{1} - {\overset{ˉ}{x}}_{1} ∥_{2} \leq h (∥ r_{1}^{d} ∥_{2} + ∥ δ_{1} ∥_{2} + ∥ τ_{1}^{B E} ∥_{2}) = O (h^{2})$ , since $r_{1}^{d} = O (h)$ and $r_{1}^{a} = O (h^{2})$ imply $δ_{1} = O (h^{2})$ by [F2]. For $h L \leq 1 / 2$ , this yields $∥ X_{1} - {\overset{ˉ}{x}}_{1} ∥_{2} = O (h^{2})$ ; [F2] and $r_{1}^{a} = O (h^{2})$ then give $∥ Z_{1} - {\overset{ˉ}{z}}_{1} ∥_{2} = O (h^{2})$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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 and Gerhard Wanner, Solving Ordinary Differential Equations II, Chapter VI §VI.1, Solving Index 1 Problems, pp. 372–381 (standard reference, not scraped)
Kendall Atkinson, Weimin Han, and David Stewart, Numerical Solution of Ordinary Differential Equations, Chapter 10 §10.4 (standard reference, not scraped)