Pipeline-generated

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.

✓ 6 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Multirate and partitioned time integration

1 · Prerequisites

2 · Summary

Summary

The frozen-slow explicit Euler scheme advances a designated slow block once per macro step and advances the fast block through explicit microsteps while holding the slow value fixed. Its evaluation count is one slow-field call and one fast-field call per microstep. A separated implementation needs the starting slow value in the fast loop and the starting fast value in the slow update; the frozen slow value can be cached, with no fast-to-slow refresh within the macro block. These counts do not imply a wall-clock speedup. Under common boundedness and Lipschitz assumptions, a direct defect and stability analysis gives fixed-time first-order convergence uniformly in the number of fast microsteps, with constants depending on the field bounds and Lipschitz constant. Explicit fast microsteps can still be unstable when the microstep is too large for the fast dynamics.

The page also proves a finite-window contraction and tail certificate for synchronous waveform Picard iteration. A separate conditional result shows how a cubic exact-start defect and one-step stability yield global order two for a symmetric exact-flow composition. Symmetry alone does not supply the cubic defect estimate. Batch 98 proves its finite-dimensional Lie and Strang splitting results under separate tube hypotheses; this conditional result does not instantiate that split map as a coupled multirate composition. Such an application would still require a specified coupling interpolant and matching defect and stability bounds.

3 · Logical flowchart

4 · Definitions, theorems and proofs

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Frozen-slow explicit Euler with fast microsteps

Definition

Let $r, s \geq 1$ , let $D \subseteq R^{r + s}$ be open, and let $f : D \to R^{r}$ and $g : D \to R^{s}$ be the designated slow and fast vector fields. The labels “slow” and “fast” are input partition labels; this definition does not assert that either field actually varies at a specified rate. The routine receives proposed state vectors $x, z$ , a real macro step $H$ , and a microstep count $m$ .

Procedure.

Before any division or field evaluation, check that $x \in R^{r}$ , $z \in R^{s}$ , $H > 0$ , $m$ is an integer with $m \geq 1$ , and $(x, z) \in D$ . If any check fails, return invalid-input.
Set $h : = H / m$ and evaluate $f (x, z)$ to set $x^{+} : = x + H f (x, z)$ .
Set $z_{0} : = z$ .
For $j = 0, 1, \dots, m - 1$ , first check whether $(x, z_{j}) \in D$ . If not, return domain-exit without a macro-step output. Otherwise evaluate $g (x, z_{j})$ and set $z_{j + 1} : = z_{j} + h g (x, z_{j})$ .
If $(x^{+}, z_{m}) \notin D$ , return domain-exit without a macro-step output. Otherwise return success and the output state $(x^{+}, z_{m})$ .

For inputs on which the procedure succeeds, write its output map as $Ψ_{H, m} (x, z) : = (x^{+}, z_{m})$ .

On a successful step the procedure uses exactly one evaluation of $f$ and $m$ evaluations of $g$ ; an invalid-input return uses no field evaluations, and a domain-exit return uses no more than these counts. The slow state is held at its initial value during every fast microstep. In a separated implementation, the slow update needs the starting fast value $z_{0}$ , while the fast loop needs the starting slow value $x$ ; $x$ can be sent to the fast worker once and cached for all $m$ microsteps, with no fast-to-slow refresh during the block. The actual communication cost depends on the implementation. The evaluation counts alone give no wall-clock saving claim, especially when the fast block accounts for nearly all right-hand-side work.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Synchronous Picard waveform relaxation on a finite window

Definition

Let $r, s \geq 1$ , $d = r + s$ , $D \subseteq R^{d}$ be open, $F = (f, g) : D \to R^{d}$ be continuous, and $u_{0} = (x_{0}, z_{0}) \in D$ . Choose a window length $Δ > 0$ , radius $R \geq 0$ , bounds $M, K \geq 0$ , tolerance $ε \geq 0$ , and integer sweep budget $B \geq 0$ . The admissibility conditions are that the closed Euclidean ball ${\overline{B}}_{R} (u_{0})$ lies in $D$ , $∥ F (u) ∥_{2} \leq M$ on that ball, $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ there, $M Δ \leq R$ , and $q : = K Δ < 1$ . If an input condition fails, return not-admissible.

Let $C_{Δ} = C ([0, Δ], R^{d})$ with $d_{\infty} (U, V) : = \sup_{0 \leq t \leq Δ} ∥ U (t) - V (t) ∥_{2}$ , and let $X_{R} : = {U \in C_{Δ} : U (0) = u_{0}, \sup_{t} ∥ U (t) - u_{0} ∥_{2} \leq R}$ . The synchronous Picard waveform map is $Φ (U) (t) : = u_{0} + \int_{0}^{t} F (U (s)) d s,$ where the vector integral is componentwise. This updates both state waveforms from the same preceding pair.

Procedure. If $B = 0$ , return the constant waveform $U^{0} (t) : = u_{0}$ with status budget-exhausted and no error certificate. Otherwise set $U^{0} (t) : = u_{0}$ and, for $k = 1, \dots, B$ , compute $U^{k} : = Φ (U^{k - 1})$ . After the first sweep set $δ_{0} : = d_{\infty} (U^{1}, U^{0})$ . After sweep $k$ , compute $E_{k} : = q^{k} δ_{0} / (1 - q)$ . If $E_{k} \leq ε$ , return $(U^{k}, tolerance-certified, E_{k}, k)$ ; if the budget is exhausted first, return $(U^{B}, budget-exhausted, E_{B}, B)$ . Integrals and waveform updates are exact mathematical operations here; quadrature and inexact subsolves require separate error terms.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Block variation bounds for a frozen-slow Euler step

Statement

Let $r, s, m$ be positive integers, $H > 0$ , $h = H / m$ , $Ω \subseteq R^{r + s}$ open, and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ be continuous. Use the product Euclidean norm $∥ (x, z) ∥_{2}^{2} = ∥ x ∥_{2}^{2} + ∥ z ∥_{2}^{2}$ . Let $S \subseteq Ω$ , and suppose $∥ F (u) ∥_{2} \leq M$ for all $u \in S$ , where $M \geq 0$ . Let $U : [0, H] \to Ω$ be an exact solution of $U^{'} = F (U)$ , and run Frozen-slow explicit Euler with fast microsteps from $U (0) = (x_{0}, z_{0})$ with $U ([0, H]) \subseteq S$ and every frozen state $(x_{0}, z_{j}) \in S$ . Then $∥ U (b) - U (a) ∥_{2} \leq M (b - a) (0 \leq a \leq b \leq H), ∥ z_{j} - z_{0} ∥_{2} \leq j h M (0 \leq j \leq m) .$

Facts & Assumptions

Given: The dimensions, macro and micro steps, field bound, exact solution, and admissible microstates in the Statement.

[F1]

View the autonomous field as $\hat{F} (t, u) : = F (u)$ on $R \times Ω$ . An exact IVP solution then satisfies its Volterra equation on every subinterval, with the value at the left endpoint as initial data (First-order systems, initial value problems, and solutions on intervals, A first-order initial value problem is equivalent to its Volterra integral equation).

[F2]

For an integrable vector field on an increasing interval, $∥ \int_{a}^{b} V (t) d t ∥_{2} \leq \int_{a}^{b} ∥ V (t) ∥_{2}$ (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).

[F3]

At each fast-loop iteration whose pre-update state $(x_{0}, z_{j})$ lies in $D$ , the procedure sets $z_{j + 1} = z_{j} + h g (x_{0}, z_{j})$ , with the same frozen $x_{0}$ at every microstep (Frozen-slow explicit Euler with fast microsteps). If all $m$ pre-update states lie in $D$ , all loop updates are performed even when the final state $(x^{+}, z_{m})$ is outside $D$ and the procedure consequently returns domain-exit.

[F4]

If an integrable real-valued function $w$ satisfies $0 \leq w \leq C$ on $[a, b]$ , then $\int_{a}^{b} w \leq C (b - a)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , claim 3).

[A1]

$U ([0, H]) \subseteq S$ and every microstate $(x_{0}, z_{j})$ belongs to $S$ , where $F$ is bounded by $M$ .

Proof

1.1F1F2F4A1algebra

Fix $0 \leq a \leq b \leq H$ . If $a = b$ , the oriented integral is zero and the bound holds. Suppose $a < b$ . Apply [F1] to the restriction of $U$ with initial time $a$ , then [F2], [A1], and [F4]: $∥ U (b) - U (a) ∥_{2} = {∥ \int_{a}^{b} F (U (t)) d t ∥}_{2} \leq \int_{a}^{b} ∥ F (U (t)) ∥_{2} d t \leq M (b - a) .$ Here $∥ F (U (t)) ∥_{2}$ is integrable by [F2] and lies between $0$ and $M$ by [A1].

2.1F3A1inductionalgebra∎

By [F3] and [A1], $∥ z_{j + 1} - z_{j} ∥_{2} = h ∥ g (x_{0}, z_{j}) ∥_{2} \leq h ∥ F (x_{0}, z_{j}) ∥_{2} \leq h M$ , since a block projection has norm at most the product norm. Starting with $z_{0} - z_{0} = 0$ and summing these $j$ increments gives $∥ z_{j} - z_{0} ∥_{2} \leq j h M$ for every $0 \leq j \leq m$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

One-step stability of frozen-slow Euler with fast microsteps

Statement

Let $r, s \geq 1$ , let $Ω \subseteq R^{r + s}$ be open, and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ . Suppose $K \geq 0$ and $F$ is jointly $K$ -Lipschitz in the product Euclidean norm on a set $S \subseteq Ω$ . Fix $T > 0$ and $0 < H \leq T$ , and let $m \geq 1$ , $h = H / m$ . For any two input states $(x, z)$ and $(\overset{ˉ}{x}, \overset{ˉ}{z})$ for which both algorithm runs return success and all inputs and fast microstates lie in $S$ , the outputs of Frozen-slow explicit Euler with fast microsteps satisfy $∥ Ψ_{H, m} (x, z) - Ψ_{H, m} (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2} \leq (1 + L_{T} H) ∥ (x, z) - (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2}, L_{T} : = K \sqrt{2 (1 + \exp (2 K T))} .$ The constant is independent of $m$ .

Facts & Assumptions

Given: The jointly $K$ -Lipschitz fields, the two admissible inputs and their fast microstates, and $0 < H \leq T$ in the Statement.

[F1]

The slow update is $x^{+} = x + H f (x, z)$ and the fast recurrence is $z_{j + 1} = z_{j} + h g (x, z_{j})$ (Frozen-slow explicit Euler with fast microsteps).

[F2]

For $u \geq 0$ , $1 + u \leq \exp (u)$ ; integer powers preserve order on nonnegative inputs; and $\exp (u + v) = \exp (u) \exp (v)$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Integer powers $a^{m}$ , The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The real exponential function and the number $e$ by a power series).

[F3]

The exponential is strictly increasing and $\exp^{'} = \exp$ ; the real mean-value theorem therefore bounds its increments on a compact interval (The exponential function is strictly increasing, The exponential function is smooth and $(\exp)^{'} = \exp$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F4]

The product Euclidean norm is $∥ (x, z) ∥_{2} = (∥ x ∥_{2}^{2} + ∥ z ∥_{2}^{2})^{1 / 2}$ ; Cauchy–Schwarz implies the Frobenius norm bounds the Euclidean operator norm of a real matrix (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[A1]

Every input and microstate used in the two successful executions lies in $S$ , and $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ for all $u, v \in S$ .

Proof

1.1F1F4A1algebra

Put $d_{x} = ∥ x - \overset{ˉ}{x} ∥_{2}$ and $d_{j} = ∥ z_{j} - {\overset{ˉ}{z}}_{j} ∥_{2}$ . By [F1] and the joint Lipschitz inequality [A1], $∥ x^{+} - {\overset{ˉ}{x}}^{+} ∥_{2} \leq (1 + K H) d_{x} + K H d_{0}$ , and $d_{j + 1} \leq (1 + h K) d_{j} + h K d_{x}$ . The second inequality uses $∥ (x, z_{j}) - (\overset{ˉ}{x}, {\overset{ˉ}{z}}_{j}) ∥_{2} \leq d_{x} + d_{j}$ .

2.1F1F2step 1.1inductionalgebra

Iterating the fast recurrence in step 1.1 gives $d_{m} \leq (1 + h K)^{m} d_{0} + ((1 + h K)^{m} - 1) d_{x}$ when $K > 0$ . For $K = 0$ it gives $d_{m} \leq d_{0}$ , the same formula at $K = 0$ . By [F2], $1 + h K \leq \exp (h K)$ ; raising nonnegative terms to the integer power $m$ and using repeated exponential addition yields $(1 + h K)^{m} \leq \exp (K H)$ . Hence $d_{m} \leq \exp (K H) d_{0} + (\exp (K H) - 1) d_{x}$ .

3.1F2F3step 1.1step 2.1algebra

If $K > 0$ , [F3] applied to $\exp$ on $[0, K H]$ gives $0 \leq η_{H} : = (\exp (K H) - 1) / H \leq K \exp (K T)$ , since its intermediate point $c$ satisfies $0 < c < K H \leq K T$ and $\exp (c) \leq \exp (K T)$ . If $K = 0$ , set $η_{H} = 0$ , and the same bound holds. Put $d = (d_{x}, d_{0})^{T}$ and $d^{+} : = (∥ x^{+} - {\overset{ˉ}{x}}^{+} ∥_{2}, ∥ z_{m} - {\overset{ˉ}{z}}_{m} ∥_{2})^{T}$ . Steps 1.1–2.1 give $d^{+} \leq (I + H B_{H}) d$ componentwise, where $B_{H} : = (\begin{array}{cc} K & K \\ η_{H} & η_{H} \end{array}), ∥ B_{H} ∥_{F} \leq \sqrt{2 K^{2} + 2 K^{2} \exp (2 K T)} = L_{T} .$

4.1F4step 3.1algebra∎

All entries of $I + H B_{H}$ are nonnegative, so componentwise domination implies $∥ d^{+} ∥_{2} \leq ∥ (I + H B_{H}) d ∥_{2}$ . By [F4], $∥ (I + H B_{H}) d ∥_{2} \leq ∥ d ∥_{2} + H ∥ B_{H} ∥_{F} ∥ d ∥_{2} \leq (1 + L_{T} H) ∥ d ∥_{2}$ . Under the product norm, $∥ d ∥_{2} = ∥ (x, z) - (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2}$ and $∥ d^{+} ∥_{2}$ is the output difference, proving the claim.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Second-order global bound under symmetric coupling and a cubic defect

Statement

Let $T > 0$ , $d \geq 1$ , let $F : Ω \to R^{d}$ be continuous on an open set $Ω \subseteq R^{d}$ , and let $Y : [0, T] \to Ω$ be an exact solution of the autonomous IVP $Y^{'} = F (Y)$ ; here exact means that $Y$ is differentiable and satisfies this equation throughout $[0, T]$ . Put $H = T / N$ with $N \geq 1$ . Let $Ψ_{H}$ be a macro map that produces one output from its current input by composing exact subsystem solution maps over subintervals with a coupling interpolant $I_{H}$ ; an exact subsystem solution map sends an initial substate to its exact value at the end of that subinterval. Define numerical states by $Y_{n + 1} = Ψ_{H} (Y_{n})$ . Here “symmetric interpolant” means $I_{H} (1 - θ; v, u) = I_{H} (θ; u, v)$ for every $θ \in [0, 1]$ and endpoint pair $u, v$ ; “symmetric step” additionally means $Ψ_{- H} = Ψ_{H}^{- 1}$ wherever both sides are defined. Assume the interpolant and macro step are symmetric in these senses, and there is a compact set $K \subseteq Ω$ containing the exact path, all numerical states, and every method stage. Suppose $∥ Y_{0} - Y (0) ∥_{2} \leq C_{0} H^{2}$ and constants $C, L \geq 0$ independent of $N$ satisfy $∥ Ψ_{H} (Y (t_{n})) - Y (t_{n + 1}) ∥_{2} \leq C H^{3}, ∥ Ψ_{H} (u) - Ψ_{H} (v) ∥_{2} \leq (1 + L H) ∥ u - v ∥_{2}$ for every $0 \leq n < N$ and all admitted inputs $u, v \in K$ . Then the global error is at most $\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^{2}$ when $L > 0$ , and at most $(C_{0} + C T) H^{2}$ when $L = 0$ . The symmetry assumptions alone do not imply the cubic defect premise.

Facts & Assumptions

Given: The exact IVP, symmetric exact-flow macro map, compact set $K$ , initial error, uniform local-defect bound, and one-step stability bound in the Statement.

[F1]

If nonnegative errors satisfy $e_{0} \leq C_{0} H^{p}$ and $e_{n + 1} \leq (1 + L H) e_{n} + C H^{p + 1}$ for $H = T / N$ , the finite recurrence bound has separate $L > 0$ and $L = 0$ forms (Finite geometric error bound from a one-step recurrence).

[F2]

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

[F3]

A first-order IVP solution is a differentiable curve satisfying its vector-field equation and initial data; for this autonomous field use $\hat{F} (t, u) = F (u)$ on $R \times Ω$ (First-order systems, initial value problems, and solutions on intervals).

[A1]

The local defect and stability inequalities hold with the same constants on all $N$ steps, and the exact path, numerical states, and method stages remain in $K$ .

Proof

1.1F2F3A1algebra

Set $e_{n} : = ∥ Y_{n} - Y (t_{n}) ∥_{2}$ for the exact solution [F3]. The Euclidean triangle inequality [F2], the local-defect premise, and the stability premise in [A1] give $e_{n + 1} \leq ∥ Ψ_{H} (Y_{n}) - Ψ_{H} (Y (t_{n})) ∥_{2} + ∥ Ψ_{H} (Y (t_{n})) - Y (t_{n + 1}) ∥_{2} \leq (1 + L H) e_{n} + C H^{3} .$

2.1A1F1step 1.1algebra∎

Apply [F1] with order $p = 2$ , step $H$ , and the stated $C_{0}, C, L$ . The initial error and recurrence from step 1.1 are exactly its hypotheses, so the $L > 0$ and $L = 0$ cases give the claimed bounds.

Remarks

The proof uses the one-step cubic defect and stability bounds. A specific Strang or other exact-flow multirate construction must establish those bounds for its actual coupling and interpolation before this corollary applies; symmetry by itself is not a local-error estimate.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Contraction and finite-sweep error bound for synchronous waveform relaxation

Statement

Let $r, s \geq 1$ and $d = r + s$ , write $u = (x, z) \in R^{r} \times R^{s}$ , and let $F = (f, g) : D \to R^{d}$ be continuous on an open set $D \subseteq R^{d}$ . Fix $u_{0} \in D$ , $Δ > 0$ , and a closed ball ${\overline{B}}_{R} (u_{0}) \subseteq D$ with radius $R \geq 0$ . Suppose $∥ F (u) ∥_{2} \leq M$ and $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ on that ball, where $M, K \geq 0$ , $M Δ \leq R$ , and $q : = K Δ < 1$ . Let $X_{R}$ be the set of continuous waveforms $U : [0, Δ] \to R^{d}$ with $U (0) = u_{0}$ and $\sup_{t} ∥ U (t) - u_{0} ∥_{2} \leq R$ , with the supremum metric, and define $Φ (U) (t) = u_{0} + \int_{0}^{t} F (U (s)) d s$ . Then $Φ : X_{R} \to X_{R}$ is a contraction with factor $q$ . It has a unique fixed point $U^{*}$ , which solves $U^{'} = F (U)$ with $U (0) = u_{0}$ . For any starting waveform $U^{0} \in X_{R}$ , if $U^{k + 1} = Φ (U^{k})$ and $δ_{0} : = ∥ U^{1} - U^{0} ∥_{\infty}$ , then $∥ U^{k} - U^{*} ∥_{\infty} \leq \frac{q^{k}}{1 - q} δ_{0} (k \geq 1) .$ Thus the finite-window algorithm certifies tolerance $ε$ after $k$ sweeps whenever this displayed bound is at most $ε$ ; budget exhaustion without that inequality supplies no such certificate.

Facts & Assumptions

Given: The domain, initial value, bounded/Lipschitz field, radius and window conditions, and waveform map in the Statement.

[F1]

Synchronous Picard waveform relaxation on a finite window: $X_{R}$ is the closed radius- $R$ set of continuous curves with initial value $u_{0}$ , and $Φ (U) (t) = u_{0} + \int_{0}^{t} F (U (s)) d s$ updates both component waveforms from the previous pair.

[F2]

Continuous $R^{d}$ -valued curves on a nonempty compact interval form a complete space in the supremum metric (Continuous $R^{n}$ -valued curves on a nonempty compact interval form a complete supremum-metric space).

[F3]

A closed subset of a complete metric space is complete in ZF, without a choice axiom (Closed subspaces of complete metric spaces are complete; the converse under countable choice, claim 2).

[F4]

For an integrable vector function on an increasing interval, $∥ \int_{a}^{b} V (s) d s ∥_{2} \leq \int_{a}^{b} ∥ V (s) ∥_{2} d s$ (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).

[F5]

The vector Riemann integral is componentwise and additive over subintervals (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). A continuous real-valued function on a compact interval is Riemann integrable, so the continuous vector integrand is componentwise integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F6]

A contraction of a nonempty complete metric space into itself has a unique fixed point, its iterates converge, and for $m \geq k$ the iterates satisfy $d (U^{m}, U^{k}) \leq q^{k} d (U^{1}, U^{0}) / (1 - q)$ (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[F7]

A continuous curve solves the first-order IVP exactly when it satisfies the associated Volterra equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[A1]

$M Δ \leq R$ and $q = K Δ < 1$ ; the stated field bounds hold throughout the closed ball.

Proof

1.1F1F2F3givenalgebra

The constant waveform $U (t) = u_{0}$ belongs to $X_{R}$ , so $X_{R}$ is nonempty. By [F2] the ambient continuous-curve space is complete. If $U_{n} \in X_{R}$ and $U_{n} \to U$ uniformly, then $U (0) = u_{0}$ and, for every $t$ , $∥ U (t) - u_{0} ∥_{2} \leq ∥ U - U_{n} ∥_{\infty} + R$ ; letting $n \to \infty$ gives $∥ U (t) - u_{0} ∥_{2} \leq R$ . Hence $X_{R}$ is closed and complete by the choice-free direction [F3].

1.2F1F4F5A1algebra

For $U \in X_{R}$ , continuity of $U$ and the field Lipschitz bound imply $∥ F (U (t)) - F (U (t_{0})) ∥_{2} \leq K ∥ U (t) - U (t_{0}) ∥_{2} \to 0$ as $t \to t_{0}$ ; this holds with one-sided limits at endpoints. Thus $F \circ U$ is continuous and componentwise integrable by [F5]. For $0 \leq s \leq t \leq Δ$ , additivity and [F4] give $∥ Φ (U) (t) - Φ (U) (s) ∥_{2} \leq M (t - s)$ ; also $Φ (U) (0) = u_{0}$ and $∥ Φ (U) (t) - u_{0} ∥_{2} \leq M t \leq M Δ \leq R$ . Thus $Φ (U) \in X_{R}$ .

1.3F1F4A1algebra

For $U, V \in X_{R}$ and $t \in [0, Δ]$ , [F4] and the field Lipschitz bound yield $∥ Φ (U) (t) - Φ (V) (t) ∥_{2} \leq \int_{0}^{t} K ∥ U (s) - V (s) ∥_{2} d s \leq K Δ ∥ U - V ∥_{\infty} = q ∥ U - V ∥_{\infty}$ . Taking the supremum proves that $Φ$ is a contraction with $q < 1$ .

2.1F1F2F3F6step 1.1step 1.2step 1.3

By [F1], [F2]–[F3], and step 1.3, [F6] applies to the nonempty complete space $X_{R}$ and the map $Φ : X_{R} \to X_{R}$ . It gives a unique fixed point $U^{*}$ and convergence of the iterates from every $U^{0} \in X_{R}$ .

3.1F1F7step 2.1

The fixed-point identity is $U^{*} (t) = u_{0} + \int_{0}^{t} F (U^{*} (s)) d s$ . By [F7], this is equivalent to the IVP $U^{'} = F (U)$ , $U (0) = u_{0}$ .

4.1F1F6step 2.1algebra∎

Fix $k \geq 1$ . By [F6], for every $m \geq k$ , $∥ U^{m} - U^{k} ∥_{\infty} \leq q^{k} δ_{0} / (1 - q)$ . Since $U^{m} \to U^{*}$ in $X_{R}$ , the triangle inequality gives $∣ ∥ U^{*} - U^{k} ∥_{\infty} - ∥ U^{m} - U^{k} ∥_{\infty} ∣ \leq ∥ U^{*} - U^{m} ∥_{\infty} \to 0$ ; passing to the limit proves the stated bound. The algorithm reports tolerance-certified only when this bound is at most $ε$ ; when the finite budget ends first, it reports budget-exhausted without claiming the requested tolerance.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Local defect bound for frozen-slow Euler with fast microsteps

Statement

Let $Ω \subseteq R^{r + s}$ be open, let $r, s \geq 1$ , and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ be continuous. Assume $K, M \geq 0$ , and that $F$ is jointly $K$ -Lipschitz and bounded by $M$ on a common set containing the exact solution $U (t) = (x (t), z (t))$ , $0 \leq t \leq H$ , and every microstate $(x_{0}, z_{j})$ of Frozen-slow explicit Euler with fast microsteps started at $U (0) = (x_{0}, z_{0})$ . Assume the exact path and those microstates lie in the domain where these bounds hold, $H > 0$ , $m \geq 1$ , and $h = H / m$ . Then the successful macro output $(x^{+}, z_{m})$ satisfies $∥ (x^{+}, z_{m}) - U (H) ∥_{2} \leq 4 K M H^{2} .$

Facts & Assumptions

Given: The exact IVP solution, jointly Lipschitz and bounded field, positive macro step, positive integer microstep count, and the common-domain conditions in the Statement.

[F1]

View the autonomous field as $\hat{F} (t, u) : = F (u)$ on $R \times Ω$ . An exact first-order IVP solution then satisfies the componentwise Volterra integral equation on every subinterval (First-order systems, initial value problems, and solutions on intervals, A first-order initial value problem is equivalent to its Volterra integral equation, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[F2]

The vector integral obeys $∥ \int_{a}^{b} V (t) d t ∥_{2} \leq \int_{a}^{b} ∥ V (t) ∥_{2} d t$ (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).

[F3]

A successful step uses $x^{+} = x_{0} + H f (x_{0}, z_{0})$ and $z_{m} = z_{0} + \sum_{j = 0}^{m - 1} h g (x_{0}, z_{j})$ (Frozen-slow explicit Euler with fast microsteps).

[F4]

Along the exact path, $∥ U (s) - U (0) ∥_{2} \leq M s$ ; for every microstate, $∥ z_{j} - z_{0} ∥_{2} \leq j h M$ (Block variation bounds for a frozen-slow Euler step).

[F5]

A coordinate projection does not increase the Euclidean norm, and $∥ (a, b) ∥_{2} \leq ∥ a ∥_{2} + ∥ b ∥_{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).

[F6]

[F7]

A continuous vector-valued function on a compact interval has continuous components, hence is componentwise integrable (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[A1]

On all points compared below, $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ and $∥ F (u) ∥_{2} \leq M$ .

Proof

1.1F1F2F3F4F5F6F7A1algebra

By [F1] and [F3], the slow coordinate defect is the integral of the continuous vector-valued integrand $f (x_{0}, z_{0}) - f (x (s), z (s))$ , integrable by [F7]. The projection bound [F5], Lipschitz condition [A1], and [F4] show its pointwise norm is at most $K M H$ . Applying [F2] and [F6] to this integrand gives $∥ x^{+} - x (H) ∥_{2} \leq K M H^{2}$ .

1.2F1F3F4F5F7algebra

By [F1] and [F3], the fast-coordinate defect is the sum over $j$ of integrals of the continuous vector-valued functions $g (x_{0}, z_{j}) - g (x (s), z (s))$ on $[j h, (j + 1) h]$ , integrable by [F7]. For such an $s$ , [F4] gives $∥ x (s) - x_{0} ∥_{2} \leq M s \leq M H$ and $∥ z (s) - z_{j} ∥_{2} \leq ∥ z (s) - z_{0} ∥_{2} + ∥ z_{j} - z_{0} ∥_{2} \leq M s + j h M \leq 2 M H$ . By [F5], the product-state distance is at most the sum of these coordinate distances, hence at most $3 M H$ .

2.1F2F5F6F7A1step 1.2algebra

The projection bound [F5] and [A1] therefore bound each fast integrand norm by $3 K M H$ . Applying [F2] and [F6] on each interval, then summing the $m$ interval norms, gives $∥ z_{m} - z (H) ∥_{2} \leq m h (3 K M H) = 3 K M H^{2}$ .

3.1F5step 1.1step 2.1algebra∎

By [F5], the product output error is at most the sum of the coordinate errors from steps 1.1 and 2.1. Thus it is at most $(1 + 3) K M H^{2} = 4 K M H^{2}$ , as claimed.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Fixed-time first-order error bound for frozen-slow Euler

Statement

Let $T > 0$ , let $Ω \subseteq R^{r + s}$ be open, $r, s \geq 1$ , and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ be continuous. Assume $K, M \geq 0$ and there is a set $S \subseteq Ω$ containing the exact path, all macro states, every fast microstate, and every method output, on which $F$ is jointly $K$ -Lipschitz and bounded by $M$ . Let $U^{'} = F (U)$ on $[0, T]$ . Take $H = T / N$ , $N \geq 1$ , and for each macro block $n$ choose an integer $m_{n} \geq 1$ and set $h_{n} = H / m_{n}$ . Starting from the exact initial value, run Frozen-slow explicit Euler with fast microsteps with these block counts and denote its macro states by $U_{n} = (x_{n}, z_{n, 0})$ . Assume every numerical step is successful and the stated bounds hold on $S$ . For each $n < N$ , also assume that the algorithm with count $m_{n}$ succeeds from the exact input $U (t_{n})$ , with all of its fast microstates and output in $S$ . Set $L_{T} : = K \sqrt{2 (1 + \exp (2 K T))} .$ Then at every macro node $t_{n} = n H$ , $∥ U_{n} - U (t_{n}) ∥_{2} \leq C_{T} H, C_{T} : = {\begin{cases} 4 K M \frac{\exp (L_{T} T) - 1}{L_{T}}, & L_{T} > 0, \\ 4 K M T, & L_{T} = 0. \end{cases}$ At each fast microstate $(x_{n}, z_{n, j})$ with $0 \leq j \leq m_{n}$ in block $n$ , its distance from the exact path at time $t_{n} + j h_{n}$ is at most $(C_{T} + 2 M) H$ . The constants do not depend on the microstep counts.

Facts & Assumptions

Given: The common set $S$ , field bounds, exact initial data, successful macro steps, and uniform fixed-time grid in the Statement.

[F1]

The frozen-slow step map is Lipschitz with factor $1 + L_{T} H$ for any two admitted inputs, uniformly in the microstep count (One-step stability of frozen-slow Euler with fast microsteps).

[F2]

An exact-start macro step has defect at most $4 K M H^{2}$ (Local defect bound for frozen-slow Euler with fast microsteps).

[F3]

If $e_{0} \leq C_{0} h^{p}$ and $e_{n + 1} \leq (1 + L h) e_{n} + C h^{p + 1}$ , the finite recurrence lemma gives the stated exponential formula for $L > 0$ and the linear formula for $L = 0$ (Finite geometric error bound from a one-step recurrence).

[F4]

[F5]

Exact-path displacement over a subinterval of length $τ$ is at most $M τ$ (Block variation bounds for a frozen-slow Euler step).

[F6]

An exact first-order IVP solution is a differentiable path satisfying $U^{'} = F (U)$ ; for this autonomous field use $\hat{F} (t, u) = F (u)$ on $R \times Ω$ (First-order systems, initial value problems, and solutions on intervals).

[F7]

On a successful macro block, the fast loop uses $z_{n, i + 1} = z_{n, i} + h_{n} g (x_{n}, z_{n, i})$ for $0 \leq i < m_{n}$ (Frozen-slow explicit Euler with fast microsteps).

[F8]

The product Euclidean norm satisfies $∥ (a, b) ∥_{2}^{2} = ∥ a ∥_{2}^{2} + ∥ b ∥_{2}^{2}$ , so each coordinate block has norm at most the full norm (Block variation bounds for a frozen-slow Euler step).

[A1]

The exact and numerical macro states, fast microstates, and method outputs lie in $S$ ; each step map comparison is admitted there and all microstep counts are positive integers.

Proof

1.1F1F2F4F6A1algebra

Put $e_{n} : = ∥ U_{n} - U (t_{n}) ∥_{2}$ for the exact solution [F6]. The triangle inequality [F4], stability [F1], and exact-start defect [F2] imply $e_{n + 1} \leq (1 + L_{T} H) e_{n} + 4 K M H^{2}$ for $0 \leq n < N$ .

2.1F3A1step 1.1algebra

Apply [F3] with $p = 1$ , $C_{0} = 0$ , $C = 4 K M$ , $L = L_{T}$ , and $h = H$ . Exact initial data gives $e_{0} = 0$ , and step 1.1 is the required recurrence. The $L_{T} > 0$ case gives $e_{n} \leq 4 K M (\exp (L_{T} T) - 1) H / L_{T}$ ; the $L_{T} = 0$ case gives $e_{n} \leq 4 K M T H$ . Taking the maximum over macro nodes proves the claimed node bound.

3.1F4F5F7F8A1step 2.1algebra∎

Fix a macro block and micro-index $j$ . By [F7] and [F8], each fast increment satisfies $∥ z_{n, i + 1} - z_{n, i} ∥_{2} = h_{n} ∥ g (x_{n}, z_{n, i}) ∥_{2} \leq h_{n} ∥ F (x_{n}, z_{n, i}) ∥_{2} \leq h_{n} M$ , since $(x_{n}, z_{n, i}) \in S$ . Summing from $i = 0$ to $j - 1$ gives $∥ z_{n, j} - z_{n, 0} ∥_{2} \leq j h_{n} M \leq H M$ ; because $x_{n}$ is frozen, this is also $∥ (x_{n}, z_{n, j}) - U_{n} ∥_{2}$ . By [F5], the exact path is at most $M j h_{n} \leq M H$ from $U (t_{n})$ . The triangle inequality [F4] and step 2.1 therefore give $∥ (x_{n}, z_{n, j}) - U (t_{n} + j h_{n}) ∥_{2} \leq e_{n} + 2 M H \leq (C_{T} + 2 M) H$ . The bound is independent of the block's microstep count, proving the stage claim.

5 · Examples, counterexamples and false statements

None yet.

Multirate and partitioned time integration

1 · Prerequisites

2 · Summary

Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Frozen-slow explicit Euler with fast microsteps

Definition

Synchronous Picard waveform relaxation on a finite window

Definition

Block variation bounds for a frozen-slow Euler step

Statement

Facts & Assumptions

Proof

One-step stability of frozen-slow Euler with fast microsteps

Statement

Facts & Assumptions

Proof

Second-order global bound under symmetric coupling and a cubic defect

Statement

Facts & Assumptions

Proof

Remarks

Contraction and finite-sweep error bound for synchronous waveform relaxation

Statement

Facts & Assumptions

Proof

Local defect bound for frozen-slow Euler with fast microsteps

Statement

Facts & Assumptions

Proof

Fixed-time first-order error bound for frozen-slow Euler

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources