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.

An index-one algebraic residual locally bounds algebraic state error

Statement

Let $K$ be a compact set of base points $(t, x)$ in a selected branch chart from A regular index-one DAE has a local reduced ODE branch, and put $z_{*} = ψ (t, x)$ . Suppose $g (t, x, \cdot)$ is $C^{2}$ on $B (z_{*}, ρ)$ for every $(t, x) \in K$ . Let $G_{*} (t, x) = g_{z} (t, x, ψ (t, x))$ . Assume common constants $γ > 0$ , $Λ \geq 0$ , and $ρ > 0$ satisfy

∥ G_{*} (t, x) v ∥_{2} \geq γ ∥ v ∥_{2} (v \in R^{m}), ∥ g_{z} (t, x, z) - G_{*} (t, x) ∥_{o p} \leq Λ ∥ z - ψ (t, x) ∥_{2}

for every $(t, x) \in K$ and $z \in B (ψ (t, x), ρ)$ ; if $Λ > 0$ , assume $ρ \leq γ / (\sqrt{m} Λ)$ . Then, uniformly for all such base points and candidates,

∥ z - z_{*} ∥_{2} \leq \frac{2}{γ} ∥ g (t, x, z) ∥_{2} .

The estimate is local: it applies only to candidates in the specified branch ball and does not turn a residual into a global branch or uniqueness certificate.

Facts & Assumptions

Given: The compact base set in a selected $C^{2}$ branch chart, the common branch radius, and the uniform lower singular-value and Jacobian-Lipschitz bounds in the Statement.

[F1]

A regular index-one DAE has a local reduced ODE branch: $g (t, x, ψ (t, x)) = 0$ on the selected local branch, and $g_{z} (t, x, ψ (t, x))$ is invertible at each base point.

[F2]

The componentwise fundamental theorem for a continuously differentiable vector path is If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz; continuity makes its derivative integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion), and For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable bounds the norm of its integral by the integral of its norm.

[F3]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm satisfies the triangle inequality.

Proof

1.1givenF1F2

Fix any $(t, x) \in K$ , put $z_{*} = ψ (t, x)$ , and set $δ = z - z_{*}$ . The branch has $m \geq 1$ algebraic variables. Since $g (t, x, z_{*}) = 0$ , apply [F2] on $s \in [0, 1]$ to the $C^{1}$ path $g (t, x, z_{*} + s δ)$ , whose segment stays in the branch ball. It gives $g (t, x, z) = G_{*} (t, x) δ + R$ , where $R = \int_{0}^{1} (g_{z} (t, x, z_{*} + s δ) - G_{*} (t, x)) δ d s$ . The anchored Jacobian bound and integral norm inequality give $∥ R ∥_{2} \leq \int_{0}^{1} Λ s ∥ δ ∥_{2}^{2} d s = (Λ / 2) ∥ δ ∥_{2}^{2} \leq (\sqrt{m} Λ / 2) ∥ δ ∥_{2}^{2}$ .

2.1givenF1F3step 1.1algebra

The common lower singular-value bound gives $∥ G_{*} (t, x) δ ∥_{2} \geq γ ∥ δ ∥_{2}$ . Using [F3] in the form $∥ G_{*} (t, x) δ + R ∥_{2} \geq ∥ G_{*} (t, x) δ ∥_{2} - ∥ R ∥_{2}$ , we obtain $∥ g (t, x, z) ∥_{2} \geq (γ - (\sqrt{m} Λ / 2) ∥ δ ∥_{2}) ∥ δ ∥_{2}$ . If $Λ > 0$ , $∥ δ ∥_{2} < ρ \leq γ / (\sqrt{m} Λ)$ makes the parenthesis at least $γ / 2$ ; if $Λ = 0$ , it equals $γ$ . In either case it is at least $γ / 2$ , with the same constants for every $(t, x) \in K$ .

3.1givenstep 2.1algebra∎

Dividing the inequality in step 2.1 by $γ / 2 > 0$ proves the asserted residual-to-state estimate for every candidate in the branch ball.

Depends on

Used by

Dependency tree · two levels

66 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.3 (standard reference, not scraped)