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 coupled index-one backward-Euler equations have a local branch

Statement

Let a compact exact solution segment lie in a common index-one branch chart with $f, g \in C^{1}$ and $g_{z}$ invertible on the graph. For each point $(t, x, ψ (t, x))$ on that segment, the coupled backward-Euler root equations

X - ξ - h f (t, X, Z) = 0, g (t, X, Z) = 0

have a unique root $(X, Z)$ in a selected neighborhood of $(x, ψ (t, x))$ whenever the step data $(h, t, ξ)$ are sufficiently close to $(0, t, x)$ . On a compact subsegment contained in one chart with positive margin, the neighborhoods and a positive step bound can be chosen uniformly after restricting the input states to that neighborhood.

Facts & Assumptions

Given: The DAE, the common branch chart, the compact reference segment, and the coupled backward-Euler residual from Finite-budget coupled backward Euler for an index-one DAE.

[F1]

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

[F2]

The parametrized implicit function theorem with $C^{k}$ regularity: a $C^{1}$ residual whose derivative in its unknown block is invertible at a zero has a unique local root branch for nearby parameters.

Proof

1.1givenF1construct

Define $Φ (h, t, ξ, X, Z) = (X - ξ - h f (t, X, Z), g (t, X, Z))$ . At $h = 0, ξ = x, X = x, Z = ψ (t, x)$ , [F1] gives $Φ = 0$ .

1.2F1algebra

The derivative of $Φ$ in the unknown pair $(X, Z)$ at this zero is the block matrix $(\begin{array}{cc} I_{d} & 0 \\ g_{x} & g_{z} \end{array})$ . If this matrix sends $(u, v)$ to zero, its first row gives $u = 0$ , and its second gives $g_{z} v = 0$ ; invertibility in [F1] gives $v = 0$ . The square matrix is therefore invertible.

2.1step 1.1step 1.2F2

Apply [F2] to $Φ$ , with $(h, t, ξ)$ as parameters and $(X, Z)$ as unknowns. It gives a unique nearby root branch for all sufficiently small parameter changes, proving the local assertion.

3.1step 2.1givenconstruct∎

The reference parameter graph ${(0, t, x (t)) : t \in [a, b]}$ is compact and lies in the open union of the IFT parameter neighborhoods from step 2.1. Compactness gives $δ > 0$ such that the $δ$ -neighborhood of this graph lies in that union. Shrink each associated unknown neighborhood inside the common branch chart. Thus, for all sufficiently small $∣ h ∣$ and input states sufficiently close to the reference graph, one IFT chart supplies the corresponding unique local root.

Depends on

Used by

Dependency tree · two levels

15 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 (standard reference, not scraped)