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 backward Euler is first 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^{2}$ . Suppose all exact and numerical states lie in a common compact branch tube, $F$ is Lipschitz in $x$ there with constant $L$ , $ψ$ is Lipschitz in $x$ with constant $L_{ψ}$ , and $f$ is Lipschitz in $z$ with constant $L_{z}$ . Assume the residual lemma's hypotheses hold uniformly on this tube: there are common $γ > 0$ , $Λ \geq 0$ , and $ρ > 0$ for its lower singular-value and Jacobian-Lipschitz bounds at every base point, with $ρ \leq γ / (\sqrt{m} Λ)$ when $Λ > 0$ ; all numerical algebraic candidates lie in the corresponding balls $B (ψ (t_{n}, X_{n}), ρ)$ . Use a uniform grid $t_{n} = n h$ , $h = T / N$ , $T > 0$ , and $N \geq 1$ . Assume the starting pair also lies in its branch ball and

∥ X_{0} - \overset{ˉ}{x} (0) ∥_{2} \leq C_{0} h, ∥ g (0, X_{0}, Z_{0}) ∥_{2} \leq C_{a, 0} h .

For each $1 \leq n \leq N$ , suppose $(X_{n}, Z_{n})$ lies in the branch ball and its coupled backward-Euler residuals satisfy

r_{n}^{d} = \frac{X_{n} - X_{n - 1}}{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, ∥ r_{n}^{a} ∥_{2} \leq C_{a} h .

Then 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

for all sufficiently small $h$ . This is a conditional accuracy result for accepted residuals; the finite-budget solver may return a failure status.

Facts & Assumptions

Given: The regular index-one DAE, a selected $C^{2}$ branch, a $C^{2}$ reduced solution on a compact tube, the Lipschitz bounds, and the stated initial and step residual bounds.

[F1]

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

[F2]

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

[F3]

Multivariable Taylor formula with a Lagrange remainder along a line segment: a $C^{2}$ function on a convex interval has its first-order Taylor expansion with a quadratic remainder.

[F4]

Finite geometric error bound from a one-step recurrence: if $e_{0} = O (h)$ and $e_{n} \leq (1 + L_{0} h) e_{n - 1} + C_{1} h^{2}$ on a uniform finite interval, then $\max_{n} e_{n} = O (h)$ .

[F5]

Backward Euler step equation and algebraic residual defines the ODE backward-Euler endpoint equation. Finite-budget coupled backward Euler for an index-one DAE defines the coupled derivative residual $r_{n}^{d} = (X_{n} - X_{n - 1}) / h - f (t_{n}, X_{n}, Z_{n})$ and algebraic residual $r_{n}^{a} = g (t_{n}, X_{n}, Z_{n})$ ; accepted candidates need not have zero residuals.

[A1]

All residuals and states satisfy the common-tube and branch-ball assumptions in the Statement, with the same $γ, Λ, ρ$ at every step.

Proof

1.1A1F2algebra

Write ${\overset{ˉ}{x}}_{n} = \overset{ˉ}{x} (t_{n})$ and ${\overset{ˉ}{z}}_{n} = ψ (t_{n}, {\overset{ˉ}{x}}_{n})$ . By [F2], the algebraic residual at each step gives $∥ Z_{n} - ψ (t_{n}, X_{n}) ∥_{2} \leq (2 C_{a} / γ) h$ . The initial pair similarly satisfies $∥ Z_{0} - ψ (0, X_{0}) ∥_{2} \leq (2 C_{a, 0} / γ) h$ .

1.2A1F1F3

Taylor's formula [F3] applied to the $C^{2}$ exact solution at $t_{n}$ gives $τ_{n} : = ({\overset{ˉ}{x}}_{n} - {\overset{ˉ}{x}}_{n - 1}) / h - F (t_{n}, {\overset{ˉ}{x}}_{n})$ with $∥ τ_{n} ∥_{2} \leq C_{τ} h$ ; one constant $C_{τ}$ works because ${\overset{ˉ}{x}}^{''}$ is bounded on the compact interval.

2.1F1step 1.1A1algebra

Put $δ_{n} = f (t_{n}, X_{n}, Z_{n}) - F (t_{n}, X_{n})$ . By [F1] and the $L_{z}$ -Lipschitz bound in $z$ , $∥ δ_{n} ∥_{2} \leq L_{z} ∥ Z_{n} - ψ (t_{n}, X_{n}) ∥_{2} \leq (2 L_{z} C_{a} / γ) h$ . The corresponding initial algebraic estimate will be used only for the final $Z_{0}$ bound.

3.1A1F1F5step 2.1step 1.2algebra

Let $e_{n} = X_{n} - {\overset{ˉ}{x}}_{n}$ . Subtracting the exact residual identity in step 1.2 from the derivative residual identity in the Statement, using the convention [F5], gives $(e_{n} - e_{n - 1}) / h = F (t_{n}, X_{n}) - F (t_{n}, {\overset{ˉ}{x}}_{n}) + δ_{n} + r_{n}^{d} - τ_{n}$ . The Lipschitz bounds and triangle inequality imply $(1 - h L) ∥ e_{n} ∥_{2} \leq ∥ e_{n - 1} ∥_{2} + h (∥ r_{n}^{d} ∥_{2} + ∥ δ_{n} ∥_{2} + ∥ τ_{n} ∥_{2})$ . For $h L \leq 1 / 2$ , $1 / (1 - h L) \leq 1 + 2 L h$ and $1 / (1 - h L) \leq 2$ , so the Statement's residual bounds and step 2.1 give $∥ e_{n} ∥_{2} \leq (1 + 2 L h) ∥ e_{n - 1} ∥_{2} + C_{2} h^{2}$ with $C_{2}$ independent of $n, h$ .

4.1F4step 3.1A1

Apply [F4] to the recurrence in step 3.1 and the initial bound $∥ e_{0} ∥_{2} \leq C_{0} h$ . It gives $\max_{n} ∥ e_{n} ∥_{2} \leq C_{3} h$ .

5.1A1F1step 1.1step 4.1algebra∎

For every $n$ , the triangle inequality and the Lipschitz bound on $ψ$ give $∥ Z_{n} - {\overset{ˉ}{z}}_{n} ∥_{2} \leq ∥ Z_{n} - ψ (t_{n}, X_{n}) ∥_{2} + L_{ψ} ∥ e_{n} ∥_{2}$ . Step 1.1 bounds the first term by a constant times $h$ , and step 4.1 bounds the second. The same argument with the initial residual bound handles $n = 0$ ; hence both state components satisfy the stated $O (h)$ bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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.2–10.3 (standard reference, not scraped)