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.

Small-step implicit Runge–Kutta stages have a unique branch and controlled residual error

Statement

Let $m, d \geq 1$ , $h > 0$ , $A \in R^{m \times m}$ , and centers $c = (c_{1}, \dots, c_{m}) \in (R^{d})^{m}$ . On block vectors define

$∥ Y ∥_{\infty, 2} : = \max_{1 \leq i \leq m} ∥ Y_{i} ∥_{2}, ∥ A ∥_{\infty} : = \max_{i} \sum_{j = 1}^{m} ∣ a_{i j} ∣ .$

Let $F : B \to (R^{d})^{m}$ , with components $F_{i} : B \to R^{d}$ , be defined on the closed product ball $B = {Y : ∥ Y - c ∥_{\infty, 2} \leq R}$ , where $R > 0$ . Suppose constants $M, L \geq 0$ satisfy, for all $Y, Z \in B$ ,

$∥ F (Y) ∥_{\infty, 2} \leq M, ∥ F (Y) - F (Z) ∥_{\infty, 2} \leq L ∥ Y - Z ∥_{\infty, 2},$

and $h ∥ A ∥_{\infty} M \leq R$ , $q : = h ∥ A ∥_{\infty} L < 1$ . Define $Φ (Y) = c + h (A \otimes I_{d}) F (Y)$ and $G (Y) = Y - Φ (Y)$ . Then $Φ$ has a unique fixed point $Y^{*} \in B$ , equivalently $G (Y^{*}) = 0$ . Every approximate stage vector $\tilde{Y} \in B$ satisfies

$∥ \tilde{Y} - Y^{*} ∥_{\infty, 2} \leq \frac{∥ G (\tilde{Y}) ∥_{\infty, 2}}{1 - q} .$

If the derivative-scaled stage residual is $r = G (\tilde{Y}) / h$ , the right side is $h ∥ r ∥_{\infty, 2} / (1 - q)$ . The hypotheses $h ∥ A ∥_{\infty} L < 1$ and the invariant-ball bound are local solvability conditions; this result gives no global branch outside $B$ .

Facts & Assumptions

Given: The finite-dimensional block space, $h, A, c, R, F, M, L$ , the product ball $B$ , and the inequalities in the Statement. The residual $G$ uses the update-residual scaling of Implicit residuals and their update and derivative units; for Runge–Kutta stages it is the block residual defined by Implicit Runge–Kutta stage equations and update.

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ defines the Euclidean inner product and norm on each $R^{d}$ .

[F2]

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

[F3]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ : every Euclidean Cauchy sequence in $R^{d}$ converges in $R^{d}$ .

[F4]

A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction from a nonempty complete metric space to itself has a unique fixed point.

[F5]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric: a metric satisfies separation, symmetry, and the triangle inequality.

[F6]

Complete metric space: every Cauchy sequence converges in the space: every Cauchy sequence in a complete metric space converges to a point of that space.

[A1]

$R > 0$ , $h ∥ A ∥_{\infty} M \leq R$ , and $q = h ∥ A ∥_{\infty} L < 1$ .

Proof

1.1givenF1F2F3F5F6construct

The formula $d (Y, Z) = ∥ Y - Z ∥_{\infty, 2}$ satisfies the metric axioms [F5]: symmetry and separation hold coordinatewise from the Euclidean norm, while the triangle inequality follows from [F2] in each block and then taking the maximum. The ball $B$ is nonempty because it contains $c$ . Any Cauchy sequence in $(B, d)$ is Cauchy in each of its $m$ Euclidean coordinates, so [F3] gives coordinate limits $Y_{i}$ . Since $∥ Y_{i} - c_{i} ∥_{2} \leq ∥ Y_{i} - Y_{i}^{(n)} ∥_{2} + ∥ Y_{i}^{(n)} - c_{i} ∥_{2}$ , passing to the limit shows $∥ Y_{i} - c_{i} ∥_{2} \leq R$ ; hence the block limit lies in $B$ . By [F6], $(B, d)$ is complete.

1.2givenA1F1F2algebra

For each block $i$ , the Euclidean triangle inequality and homogeneity give $∥ \sum_{j} a_{i j} F_{j} (Y) ∥_{2} \leq \sum_{j} ∣ a_{i j} ∣ ∥ F_{j} (Y) ∥_{2} \leq (\sum_{j} ∣ a_{i j} ∣) M$ ; taking the maximum over $i$ gives $∥ Φ (Y) - c ∥_{\infty, 2} \leq h ∥ A ∥_{\infty} M \leq R$ , so $Φ (Y) \in B$ . Applying the same blockwise estimate to $F (Y) - F (Z)$ gives $∥ Φ (Y) - Φ (Z) ∥_{\infty, 2} \leq h ∥ A ∥_{\infty} L ∥ Y - Z ∥_{\infty, 2} = q ∥ Y - Z ∥_{\infty, 2}$ .

2.1step 1.1step 1.2F4

The hypotheses of [F4] hold by step 1.1 and step 1.2, so there is exactly one $Y^{*} \in B$ with $Φ (Y^{*}) = Y^{*}$ . The equation $Φ (Y^{*}) = Y^{*}$ is equivalent to $G (Y^{*}) = 0$ by the definition of $G$ .

3.1A1step 1.2step 2.1algebra∎

For any $\tilde{Y} \in B$ , $G (\tilde{Y}) = \tilde{Y} - Φ (\tilde{Y})$ and $Y^{*} = Φ (Y^{*})$ , so $∥ \tilde{Y} - Y^{*} ∥_{\infty, 2} \leq ∥ G (\tilde{Y}) ∥_{\infty, 2} + ∥ Φ (\tilde{Y}) - Φ (Y^{*}) ∥_{\infty, 2} \leq ∥ G (\tilde{Y}) ∥_{\infty, 2} + q ∥ \tilde{Y} - Y^{*} ∥_{\infty, 2}$ . Since $1 - q > 0$ , rearranging proves the stated residual-to-stage-error bound, and $G (\tilde{Y}) = h r$ proves the derivative-scaled form.

Depends on

Used by

Dependency tree · two levels

53 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, Introduction à l’Analyse Numérique, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)
John C. Butcher, Implicit Runge–Kutta Methods, tutorial accompanying Numerical Methods for Ordinary Differential Equations (standard reference, not scraped)