TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Global error from uniform one-step defect and stability

Statement

Let $d, N, p \geq 1$ , $T > 0$ , $h = T / N$ , and $t_{n} = n h$ . Let $y : [0, T] \to R^{d}$ solve an initial-value problem in an open time-state domain $D$ . Use the Euclidean norm $∥ v ∥_{2} = (\sum_{i = 1}^{d} v_{i}^{2})^{1 / 2}$ of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , whose triangle inequality is proved in Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation. Let $T \subset D$ be a common compact time-state tube with positive margin in $D$ , and write $T_{t} : = {v \in R^{d} : (t, v) \in T}$ . Suppose a one-step map $Ψ_{h, n}$ is defined on $T_{t_{n}}$ , produces $y_{n + 1} = Ψ_{h, n} (y_{n})$ , and the entire exact path, all numerical grid states, and every method stage lie in $T$ . If constants $C, C_{0}, L \geq 0$ , independent of $N$ and $n$ , satisfy $∥ y_{0} - y (0) ∥_{2} \leq C_{0} h^{p}, ∥ Ψ_{h, n} (y (t_{n})) - y (t_{n + 1}) ∥_{2} \leq C h^{p + 1},$ and $∥ Ψ_{h, n} (u) - Ψ_{h, n} (v) ∥_{2} \leq (1 + L h) ∥ u - v ∥_{2}$ for every $u, v \in T_{t_{n}}$ and $0 \leq n < N$ , then, for $L > 0$ , $\max_{0 \leq n \leq N} ∥ y_{n} - y (t_{n}) ∥_{2} \leq (C_{0} \exp (L T) + C \frac{\exp (L T) - 1}{L}) h^{p},$ and, for $L = 0$ , $\max_{0 \leq n \leq N} ∥ y_{n} - y (t_{n}) ∥_{2} \leq (C_{0} + C T) h^{p} .$

Facts & Assumptions

Given: An exact first-order initial-value problem, the stated one-step map and tube, and the local-defect, stability, and initial-error bounds.

[F1]

A solution of a first-order system satisfies $x (t_{0}) = x_{0}$ and $x^{'} (t) = F (t, x (t))$ on its interval (First-order systems, initial value problems, and solutions on intervals).

[F2]

For a one-step map, the local defect is the difference between its exact-start output and the exact next state; uniform local order $p$ bounds its norm by $C h^{p + 1}$ , and one-step Lipschitz stability bounds changes in the output by $(1 + L h)$ times the input change (One-step ODE methods, local defect, uniform order, and step stability).

[F3]

The Euclidean norm on $R^{d}$ satisfies $∥ u + v ∥_{2} \leq ∥ u ∥_{2} + ∥ v ∥_{2}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F4]

$\exp$ is the real exponential defined by its factorial power series, with $e : = \exp (1)$ (The real exponential function and the number $e$ by a power series).

[L1]

For $h = T / N$ and $e_{n + 1} \leq (1 + L h) e_{n} + C h^{p + 1}$ with $e_{0} \leq C_{0} h^{p}$ , the finite recurrence has the two bounds stated in this item's conclusion (Finite geometric error bound from a one-step recurrence).

[A1]

The one-step map is defined on each stated time fiber, the entire exact path, numerical grid states and method stages remain in $T$ , and its uniform local defect and fiberwise stability inequalities in the Statement hold.

Proof

1.1F1F2F3A1algebra

By [F1], each $y (t_{n})$ is a defined reference state of the exact initial-value problem; [F2] identifies the two uniform inequalities in [A1] as the one-step stability and local-defect bounds. Put $e_{n} : = ∥ y_{n} - y (t_{n}) ∥_{2}$ . The Euclidean triangle inequality [F3] and those bounds give $e_{n + 1} \leq ∥ Ψ_{h, n} (y_{n}) - Ψ_{h, n} (y (t_{n})) ∥_{2} + ∥ Ψ_{h, n} (y (t_{n})) - y (t_{n + 1}) ∥_{2} \leq (1 + L h) e_{n} + C h^{p + 1}$ .

2.1A1F4L1step 1.1∎

Apply [L1] to the nonnegative sequence $(e_{n})_{n = 0}^{N}$ using the recurrence from step 1.1 and the initial bound in [A1]. The two cases $L > 0$ and $L = 0$ give exactly the displayed conclusions, with exponential notation as in [F4].

Depends on

Used by

Dependency tree · two levels

38 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)
Mark Embree, Lecture Notes on Numerical Analysis (standard reference, not scraped)