TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

IMEX Euler has a first-order local defect and a one-step stability bound

Statement

Let $d \geq 1$ and let $F = a + b$ on an open set $U \subseteq R^{d}$ as in Additive autonomous ODE partitions. On a common compact convex tube $T \subset U$ , suppose $a, b$ are bounded and Lipschitz with constants $M_{a}, M_{b}, L_{a}, L_{b}$ . For every $u \in T$ and sufficiently small $h > 0$ , assume there is a closed ball $\overline{B} (c_{u}, R_{u}) \subset T$ with $R_{u} > 0$ , centered at $c_{u} : = u + h a (u)$ , and with $h M_{b} \leq R_{u}$ ; the branch lemma then gives a unique root $Ψ_{h} (u) = c_{u} + h b (Ψ_{h} (u))$ in that ball when $h L_{b} \leq 1 / 2$ . Require that the exact solution segment from each reference state $y (t) \in T$ stays in $T$ and that its endpoint $y (t + h)$ lies in $\overline{B} (c_{y (t)}, R_{y (t)})$ . Then, uniformly on the tube, $∥ Ψ_{h} (y (t)) - y (t + h) ∥_{2} \leq C h^{2}, ∥ Ψ_{h} (u) - Ψ_{h} (v) ∥_{2} \leq (1 + L h) ∥ u - v ∥_{2},$ where one may take $L = 2 (L_{a} + L_{b})$ and $C$ depends only on the stated tube bounds and branch margins. The local defect is therefore $O (h^{2})$ , and the exact-root method is first order locally.

Facts & Assumptions

Given: The additive IVP, a common tube with uniform field bounds, the positive-radius branch balls and branch hypotheses for every starting state in that tube, exact path segments and endpoints admitted in their branch balls, and $h L_{b} \leq 1 / 2$ .

[F1]

One-step IMEX Euler with an implicit branch and residual status: the exact update is $Y = y + h a (y) + h b (Y)$ .

[F2]

A local IMEX Euler branch from contraction: if $∥ b ∥ \leq M_{b}$ , $b$ is $L_{b}$ -Lipschitz on the selected ball, $h M_{b} \leq R$ , and $h L_{b} < 1$ , the exact branch exists uniquely and satisfies the residual-to-root bound.

[F3]

Along each exact solution segment in $T$ , $s \mapsto F (y (s))$ is continuous because $F$ is Lipschitz on $T$ and $y$ is continuous. Each coordinate is therefore integrable on the compact segment (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion), so the vector derivative is integrable; the vector-valued fundamental theorem of calculus (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz) gives $y (t + s) - y (t) = \int_{0}^{s} F (y (t + r)) d r$ .

[F4]

For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable: for an integrable vector function on an increasing interval, $∥ \int f ∥_{2} \leq \int ∥ f ∥_{2}$ .

[A1]

$F = a + b$ is bounded by $M_{F} : = M_{a} + M_{b}$ and Lipschitz with $L_{F} : = L_{a} + L_{b}$ on the tube; the exact path and its endpoints remain in the stated convex tube, and each selected root belongs to its stated branch ball in that tube.

Proof

1.1A1F3F4algebra

By [F3], for $0 \leq s \leq h$ , $ϕ_{s} - y = \int_{0}^{s} F (ϕ_{r}) d r$ , so [F4] and [A1] give $∥ ϕ_{s} - y ∥_{2} \leq M_{F} s$ . Subtracting $h F (y)$ from the integral at $h$ and applying [F4] again yields $∥ ϕ_{h} - y - h F (y) ∥_{2} \leq \int_{0}^{h} L_{F} ∥ ϕ_{s} - y ∥_{2} d s \leq \frac{1}{2} L_{F} M_{F} h^{2}$ .

2.1A1F1F2step 1.1algebra

Set $c = y + h a (y)$ and evaluate the implicit residual of the exact endpoint: $r_{ϕ} : = ϕ_{h} - c - h b (ϕ_{h}) = (ϕ_{h} - y - h F (y)) - h (b (ϕ_{h}) - b (y))$ . By [A1] and step 1.1, $∥ r_{ϕ} ∥_{2} \leq M_{F} (\frac{1}{2} L_{F} + L_{b}) h^{2}$ . The exact endpoint and the branch root lie in the same admitted branch ball, so [F2] gives $∥ Ψ_{h} (y) - ϕ_{h} ∥_{2} \leq 2 M_{F} (\frac{1}{2} L_{F} + L_{b}) h^{2}$ .

3.1A1F1algebra∎

For two inputs $u, v$ with selected roots $Y_{u}, Y_{v}$ , subtracting their equations in [F1] and using the Lipschitz bounds gives $(1 - h L_{b}) ∥ Y_{u} - Y_{v} ∥_{2} \leq (1 + h L_{a}) ∥ u - v ∥_{2}$ . Since $h L_{b} \leq 1 / 2$ , $(1 + h L_{a}) / (1 - h L_{b}) = 1 + h (L_{a} + L_{b}) / (1 - h L_{b}) \leq 1 + 2 (L_{a} + L_{b}) h$ . This is the stated one-step stability bound.

Depends on

Used by

Dependency tree · two levels

65 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

Uri M. Ascher, Steven J. Ruuth, and Raymond J. Spiteri, Implicit-explicit Runge-Kutta methods for time-dependent partial differential equations (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)