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.

✓ 3 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; all 3 also cleared it.

Multirate and partitioned time integration — Examples

1 · Prerequisites

2 · Summary

These examples compute a dissipative linear electromechanical model with slow mechanical and fast electrical blocks, a stable coupled linear system whose explicit fast Euler microstep expands perturbations, and a scalar slow-fast model where freezing the slow waveform creates a terminal first-order error. The final example calculates a midpoint-sampled alternative that is exact only for that model; it does not verify the separate symmetric-composition interface.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A dissipative electromechanical toy model under slow-fast blocking

Example

Use the linear toy model with mechanical position $q$ , velocity $v$ , and electrical current $i$ : $q^{'} = v, v^{'} = - q - v + i, i^{'} = v - 8 i .$ The unit mass, unit spring and damping coefficients, unit inductance, resistance $8$ , force-current coupling, and back-emf coupling are stipulated model data. Its mechanical block is $x = (q, v)$ and its electrical block is $z = i$ . For the quadratic energy $E (q, v, i) = \frac{1}{2} (q^{2} + v^{2} + i^{2})$ , $E^{'} = - (v - i)^{2} - 7 i^{2} \leq 0.$ Thus the exact model dissipates this energy. Starting from $(q, v, i) = (0, 1, 0)$ , apply Frozen-slow explicit Euler with fast microsteps with $H = 1 / 10$ , $m = 4$ , and $h = 1 / 40$ . The macro method returns $(q^{+}, v^{+}, i_{4}) = (1 / 10, 9 / 10, 369 / 5000)$ .

Facts & Assumptions

Given: The stipulated electromechanical model, initial state, macro step $H = 1 / 10$ , and four fast microsteps of length $h = 1 / 40$ .

[F1]

The assigned algorithm updates the slow block once by explicit Euler and then updates the fast block four times while keeping the slow state fixed at its initial value (Frozen-slow explicit Euler with fast microsteps).

[F2]

If $E$ is continuous on $[t_{1}, t_{2}]$ and differentiable on $(t_{1}, t_{2})$ , then $E (t_{2}) - E (t_{1}) = E^{'} (c) (t_{2} - t_{1})$ for some $c \in (t_{1}, t_{2})$ (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)$ ).

[A1]

In this example $f (q, v, i) = (v, - q - v + i)$ and $g (q, v, i) = v - 8 i$ ; the mechanical and electrical labels refer to this stipulated block partition.

Proof

1.1A1F2algebra

Differentiating $E = \frac{1}{2} (q^{2} + v^{2} + i^{2})$ along [A1] gives $E^{'} = q v + v (- q - v + i) + i (v - 8 i) = - v^{2} + 2 v i - 8 i^{2} = - (v - i)^{2} - 7 i^{2} \leq 0$ . On any solution interval and any $t_{1} < t_{2}$ , [F2] gives $E (t_{2}) - E (t_{1}) = E^{'} (c) (t_{2} - t_{1}) \leq 0$ , so the energy is nonincreasing.

1.2F1A1algebra

By [F1] and [A1], the mechanical update uses the initial state $(q, v, i) = (0, 1, 0)$ : $q^{+} = 0 + (1 / 10) 1 = 1 / 10$ and $v^{+} = 1 + (1 / 10) (- 0 - 1 + 0) = 9 / 10$ .

1.3F1A1inductionalgebra

The fast recurrence uses frozen $v = 1$ , so $i_{j + 1} = i_{j} + (1 / 40) (1 - 8 i_{j})$ . Starting with $i_{0} = 0$ , successive substitution gives $i_{1} = 1 / 40$ , $i_{2} = 9 / 200$ , $i_{3} = 61 / 1000$ , and $i_{4} = 369 / 5000$ . Thus the stated macro output follows.

2.1F1step 1.2step 1.3algebra∎

By [F1], the method evaluates the two-component mechanical field once and the electrical field four times. Its fast loop reads the initial slow value $v = 1$ at each stage, so an implementation may transmit that frozen value once at the block boundary and cache it; no fast-to-slow refresh occurs inside this macro block. This count describes the procedure and does not claim a wall-clock saving.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A stable coupled model has an unstable explicit fast microstep

Example

Consider $x^{'} = - x$ , $z^{'} = x - 8 z$ from $(x_{0}, z_{0}) = (1, 1)$ . Its exact solution for arbitrary initial data is $x (t) = x_{0} e^{- t}, z (t) = e^{- 8 t} z_{0} + \frac{x_{0}}{7} (e^{- t} - e^{- 8 t}) .$ It tends to zero as $t \to \infty$ , so the continuous linear system is asymptotically stable, meaning every solution tends to the origin. Apply Frozen-slow explicit Euler with fast microsteps with $H = 3 / 5$ , $m = 2$ , and $h = 3 / 10$ . The method gives $x^{+} = 2 / 5$ , $z_{1} = - 11 / 10$ , and $z_{2} = 46 / 25$ . At fixed frozen $x$ , a fast-coordinate perturbation is multiplied per microstep by $1 - 8 h = - 7 / 5$ , whose magnitude exceeds one; the exact homogeneous fast perturbation instead decays.

Facts & Assumptions

Given: The linear vector field, initial data, macro step, and microstep count specified above.

[F1]

The assigned algorithm updates the slow coordinate once by explicit Euler and then performs $m$ fast Euler updates using the original frozen slow state (Frozen-slow explicit Euler with fast microsteps).

[F2]

The exponential satisfies $e^{0} = 1$ and $e^{a + b} = e^{a} e^{b}$ , has derivative $e^{t}$ , is increasing, and obeys $1 + t \leq e^{t}$ for $t \geq 0$ (The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential function is strictly increasing, The exponential function is smooth and $(\exp)^{'} = \exp$ , $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ).

[A1]

In this example $f (x, z) = - x$ and $g (x, z) = x - 8 z$ .

Proof

1.1F2A1algebra

Differentiating the displayed formula with [F2] gives $x^{'} = - x$ and $z^{'} = x - 8 z$ , and at $t = 0$ it gives the arbitrary initial pair $(x_{0}, z_{0})$ . Thus it is the exact solution. For $t \geq 0$ , [F2] gives $e^{t} \geq 1 + t > 0$ and $e^{8 t} \geq 1 + 8 t > 0$ , while the addition formula gives $e^{- t} = 1 / e^{t}$ and $e^{- 8 t} = 1 / e^{8 t}$ . Therefore $0 < e^{- t} \leq 1 / (1 + t)$ and $0 < e^{- 8 t} \leq 1 / (1 + 8 t)$ . Given $ε > 0$ , both bounds are below $ε$ whenever $t > \max {1 / ε, 1 / (8 ε)}$ , so both exponentials and then both solution components tend to zero.

1.2F1F2A1algebra

By [F1] and [A1], $x^{+} = 1 + (3 / 5) (- 1) = 2 / 5$ . The fast updates use frozen $x = 1$ , so $z_{1} = 1 + (3 / 10) (1 - 8) = - 11 / 10$ and $z_{2} = - 11 / 10 + (3 / 10) (1 - 8 (- 11 / 10)) = 46 / 25$ . Subtracting two fast recurrences with the same frozen $x$ gives $δ z_{j + 1} = (1 - 8 h) δ z_{j} = - 7 / 5 δ z_{j}$ . The exact homogeneous fast equation $w^{'} = - 8 w$ has solution $w (t) = e^{- 8 t} w (0)$ by [F2]. Since $e^{8 h} \geq 1 + 8 h > 1$ , its reciprocal $e^{- 8 h}$ lies in $(0, 1)$ , so the exact homogeneous multiplier decays.

2.1F1step 1.1step 1.2algebra∎

Step 1.1 directly shows every exact solution tends to zero, whereas step 1.2 gives an expanding fast perturbation in each explicit microstep. The successful step costs one $f$ and two $g$ evaluations, which by itself makes no wall-clock speedup claim.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Freezing a varying slow waveform leaves a first-order coupling error

Example

Consider $x^{'} = 1$ , $z^{'} = x$ , $(x_{0}, z_{0}) = (0, 0)$ on $[0, T]$ , with $T > 0$ and $N \geq 1$ equal macro steps $H = T / N$ . The exact solution is $x (t) = t$ , $z (t) = t^{2} / 2$ . The frozen-slow method Frozen-slow explicit Euler with fast microsteps has $x_{n} = n H$ and $z_{N} = T^{2} / 2 - T H / 2$ , so its terminal $z$ error is $T H / 2$ . For any integer $m \geq 1$ , set $h = H / m$ and instead update each midpoint-sampled block by $z_{n, 0} = z_{n}$ and $z_{n, j + 1} = z_{n, j} + h (x_{n} + (j + \frac{1}{2}) h)$ for $0 \leq j < m$ . Then one macro update adds exactly $H x_{n} + H^{2} / 2$ , and this alternative gives the exact solution at every macro node for this model. This is a model-specific diagnostic, not a claim about any unverified symmetric composition.

Facts & Assumptions

Given: The model, initial values, $T > 0$ , and integer $N \geq 1$ in the Example.

[F1]

The frozen-slow algorithm sets $x^{+} = x + H f (x, z)$ and uses the original $x$ during its fast updates $z_{j + 1} = z_{j} + h g (x, z_{j})$ (Frozen-slow explicit Euler with fast microsteps).

[A1]

Here $f (x, z) = 1$ , $g (x, z) = x$ , and $H = T / N$ .

Proof

1.1F1A1inductionalgebra

Direct integration gives $x (t) = t$ and $z (t) = t^{2} / 2$ . By [F1] and [A1], induction on $n$ gives $x_{n} = n H$ ; because $g (x_{n}, z) = x_{n}$ is constant across a frozen block, $z_{n + 1} = z_{n} + H x_{n}$ . Starting with $z_{0} = 0$ , summation gives $z_{N} = H^{2} \sum_{n = 0}^{N - 1} n = H^{2} N (N - 1) / 2 = T^{2} / 2 - T H / 2$ , so the terminal error is $T H / 2 > 0$ .

2.1A1step 1.1algebra∎

Under midpoint sampling, the fast block increment is $\sum_{j = 0}^{m - 1} h (x_{n} + (j + \frac{1}{2}) h) = H x_{n} + h^{2} \sum_{j = 0}^{m - 1} (j + \frac{1}{2}) = H x_{n} + H^{2} / 2$ , since $m h = H$ and $\sum_{j = 0}^{m - 1} (j + \frac{1}{2}) = m^{2} / 2$ . If $z_{n} = (n H)^{2} / 2$ , this increment gives $z_{n + 1} = ((n + 1) H)^{2} / 2$ ; with $z_{0} = 0$ , induction proves exactness at every macro node.