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.

The finite-budget index-one DAE solvers return a status in finite work

Statement

In the exact-arithmetic model with returning residual, Jacobian, domain-test and correction primitives, suppose the initialization and stepper algorithms in Finite-budget index-one DAE consistent initialization, Finite-budget coupled backward Euler for an index-one DAE, and Finite-budget coupled constant-step BDF2 for an index-one DAE are run with finite grid length and finite Newton budget $B$ . Count explicit residual queries separately from work internal to Jacobian assembly and linear-system backends. Each call returns a status after finitely many such queries. A Newton call makes at most $B$ correction calls and $B + 1$ explicit residual evaluations. Initialization makes at most one additional algebraic-residual evaluation after a root status to record the returned residual norm, so it uses at most $B + 2$ evaluations. A backward-Euler call with $S$ attempted steps uses at most $1 + S (B + 2)$ residual evaluations, including its one starting algebraic-residual check; a BDF2 call with $S$ attempted steps uses at most $2 + S (B + 2)$ , including its two starting algebraic-residual checks. These bounds include calls that return early with a failure status. Every successful correction solves one current Jacobian system, of dimension $m$ in initialization and $d + m$ in either stepper; assembly and solve costs depend on the backend.

For either stepper, every appended candidate satisfies $∥ r_{n}^{d} ∥_{2} \leq η_{d}$ and $∥ r_{n}^{a} ∥_{2} \leq η_{a}$ for its defined derivative and algebraic residuals. These are conditional accepted-residual bounds. No residual tolerance is guaranteed to be attained, and these bounds assert neither an exact zero, uniqueness nor a discretization error estimate.

Facts & Assumptions

Given: The finite grids, finite correction budget, exact loops and status branches in the three DAE algorithms, and the returning-primitive convention in the Statement.

[F1]

Finite-budget Newton preserves its domain and returns a status in bounded outer work: with budget $B$ , an admissible Newton call makes at most $B$ correction calls and $B + 1$ explicit residual evaluations and returns a stated status under the returning-primitive convention.

[F2]

Finite-budget index-one DAE consistent initialization: initialization makes one such Newton call in $m$ algebraic unknowns and, on root status, one extra algebraic-residual evaluation.

[F3]

Finite-budget coupled backward Euler for an index-one DAE: the wrapper checks one starting algebraic residual and checks the previous-state seed against the open slice $T_{t_{n}}$ before each Newton call, returning invalid-trial with the computed prefix if that check fails. Otherwise it calls Newton once with budget $B$ , tolerance $1$ and scaled residual $R_{n} = (r_{n}^{d} / η_{d}, r_{n}^{a} / η_{a})$ on that slice. It reevaluates the unscaled block residual once after a root status and returns immediately on any non-root status. The unknown has dimension $d + m$ .

[F4]

Finite-budget coupled constant-step BDF2 for an index-one DAE: the wrapper checks both starting algebraic residuals and checks its extrapolated seed against the open slice $T_{t_{n}}$ before each Newton call, returning invalid-trial with the computed prefix if that check fails. Otherwise it calls Newton once with budget $B$ , tolerance $1$ and scaled residual $R_{n} = (r_{n}^{d} / η_{d}, r_{n}^{a} / η_{a})$ on that slice. It reevaluates the unscaled block residual once after a root status and returns immediately on any non-root status. The unknown has dimension $d + m$ .

Proof

1.1givenF1F2F3F4

Apply the proved work bound [F1] to each admissible Newton call. It gives at most $B + 1$ explicit residual evaluations and $B$ correction calls. The exact procedure Finite-budget Newton for a square vector residual passes its current Jacobian and residual to the correction routine; a successful correction solves that single square system. The input dimensions in [F2]–[F4] are $m$ and $d + m$ , respectively, giving the asserted system dimensions. This does not bound assembly or solve costs.

2.1F1F2step 1.1

Initialization makes one Newton call by [F2]. If it returns a non-root status, the wrapper returns immediately; if it returns root, it reevaluates the algebraic residual once to distinguish exact from approximate consistency. Thus it uses at most $B + 2$ residual evaluations.

2.2F1F3F4step 1.1algebra

A backward-Euler call first evaluates its starting algebraic residual once, and a BDF2 call evaluates its two starting algebraic residuals, by [F3] and [F4]. Thus their preliminary checks use at most one and two evaluations, respectively, even when a bound fails. Each attempted step makes at most one Newton call; on a root status the wrapper reevaluates the block residual once to record the unscaled blocks, and otherwise returns immediately. Each attempted step therefore adds at most $B + 2$ evaluations. Summing gives $1 + S (B + 2)$ for backward Euler and $2 + S (B + 2)$ for BDF2. The pre-call membership tests add no residual evaluation, and all loops and tests are finite.

3.1givenstep 1.1step 2.1step 2.2

All remaining tests, assignments and arithmetic are finite under the returning-primitive convention. The argument therefore proves termination without assuming that Newton converges or accepts a step.

4.1givenF3F4algebra∎

For each appended candidate, [F3] or [F4] gives a Newton root status with tolerance $1$ . The procedure's residual test gives $∥ R_{n} ∥_{2} \leq 1$ . In both methods its blocks equal $r_{n}^{d} / η_{d}$ and $r_{n}^{a} / η_{a}$ . Each block norm is at most the concatenated Euclidean norm, and both tolerances are positive; hence $∥ r_{n}^{d} ∥_{2} \leq η_{d}$ and $∥ r_{n}^{a} ∥_{2} \leq η_{a}$ . No other solver status supplies this premise.

Depends on

Used by

Nothing in the library uses this result yet.

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)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Julia edition, §4.5 Newton for nonlinear systems (standard reference, not scraped)