TheoremStatement: 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.

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]

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).

[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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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

Michael Günther and Adrian Sandu, Multirate Methods for Ordinary Differential Equations, CSL-TR-25-5 (2025) (standard reference, not scraped)
Mark Embree, Lecture Notes on Numerical Analysis, Lecture 34: Global Analysis of One-Step Integrators (2016) (standard reference, not scraped)