LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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 two implicit ARS stages have selected branches and residual bounds

Statement

Let $γ = 1 - 1 / \sqrt{2}$ as in The ARS(2,2,2) additive tableau and its three stages. For each of the two implicit stages, let $c_{j}$ be its center after the previous stages have been selected. Suppose $b$ is bounded by $M$ and $L$ -Lipschitz on a closed ball $\overline{B} (c_{j}, R_{j}) \subset U$ with $R_{j} > 0$ , and $∣ γ ∣ h M \leq R_{j}$ , $∣ γ ∣ h L < 1$ . Then stage $Y_{j} = c_{j} + γ h b (Y_{j})$ has a unique root in that ball. Every candidate ${\tilde{Y}}_{j}$ in the same ball with unscaled stage-equation residual $r_{j}$ satisfies $∥ {\tilde{Y}}_{j} - Y_{j} ∥_{2} \leq \frac{∥ r_{j} ∥_{2}}{1 - ∣ γ ∣ h L} .$ The claim is local to these stage balls; it asserts no remote-root or large-step branch.

Facts & Assumptions

Given: The ARS(2,2,2) coefficients, $h > 0$ , and for each sequential stage its center, positive-radius closed ball, bounds $M, L$ , and the two small-step inequalities.

[F1]

The ARS(2,2,2) additive tableau and its three stages: $Y_{2} = c_{2} + γ h b (Y_{2})$ with $c_{2} = y + γ h a (y)$ ; after selecting $Y_{2}$ , $Y_{3} = c_{3} + γ h b (Y_{3})$ with $c_{3} = y + h [δ a (y) + (1 - δ) a (Y_{2}) + (1 - γ) b (Y_{2})]$ .

[F2]

Small-step implicit Runge–Kutta stages have a unique branch and controlled residual error: on an invariant product ball, if $h ∥ A ∥_{\infty} M \leq R$ and $h ∥ A ∥_{\infty} L < 1$ , the implicit stages have a unique fixed point and the unscaled residual bounds the stage error by the reciprocal contraction margin.

[A1]

The two balls are admitted in $U$ , $b$ has the stated bounds on each, and $∣ γ ∣ h M \leq R_{j}$ , $∣ γ ∣ h L < 1$ for $j = 2, 3$ .

Proof

1.1A1F1F2algebra

For stage two in [F1], apply [F2] to the one-stage matrix $A = [γ]$ , the one-block function $F_{1} = b$ , and center $c_{2}$ ; its matrix row norm is $∥ A ∥_{\infty} = ∣ γ ∣$ , so [A1] gives the invariant-ball and contraction hypotheses. Hence the second stage root exists uniquely, and its residual bound is the one in [F2], with contraction factor $∣ γ ∣ h L$ .

2.1A1F1F2step 1.1

With that selected $Y_{2}$ , the third-stage center $c_{3}$ in [F1] is fixed. Apply [F2] again to the one-stage matrix $[γ]$ , function $b$ , and ball centered at $c_{3}$ ; [A1] verifies the same hypotheses, giving a unique $Y_{3}$ and its residual bound with contraction factor $∣ γ ∣ h L$ .

3.1step 1.1step 2.1∎

The stages are solved in order, so step 1.1 determines the center used in step 2.1. Both roots are unique in their selected balls, and the residual estimates hold for every candidate in those balls; no statement is made outside them.

Depends on

Used by

The ARS(2,2,2) pair is second order under distinct stage residual tolerances Theorem

Dependency tree · two levels

13 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, Introduction à l’Analyse Numérique, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)
Lorenzo Pareschi and Giovanni Russo, Implicit-explicit Runge-Kutta schemes and applications to hyperbolic systems with relaxation (standard reference, not scraped)