ExampleConstruction: AI-generatedVerification: 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.

Too few sweeps lower the order from Gauss collocation

Example

Assume Countable Choice for the Lebesgue interval-measure formula. Apply one-node Gauss SDC to $y^{'} = y$ , $y (0) = 1$ , on $[0, 1]$ , using the constant predictor, fixed stopping tolerance $t o l = 1$ , and a sweep budget $K \geq 1$ . For sufficiently small uniform steps, the first residual check accepts the uncorrected predictor at every step.

Facts & Assumptions

Given: The one-node Gauss tableau, explicit-left-Euler SDC sweep, constant predictor, unit tolerance, a budget $K \geq 1$ , uniform mesh $h = 1 / N$ , and the supplied flag invariance_certified=true; step 1.1 verifies its guarantee.

[F1]

Finite explicit-left-Euler spectral deferred-correction sweep: the first update uses $Q_{Δ} = 0$ for one node, computes $U^{1}$ , and returns $U^{0}$ if $∥ U^{1} - U^{0} ∥ \leq (1 - q) t o l$ .

[F2]

One-node Gauss collocation is implicit midpoint of order two: the fully solved one-node Gauss method is implicit midpoint and has global order two on the stated smooth tube.

[F3]

Each SDC sweep raises the order up to the collocation order: a fixed candidate $U^{k}$ from a constant predictor has the guaranteed global-error bound $O (h^{\min (1, k + 1)})$ when used as the one-node method under its hypotheses. For $U^{0}$ this is an $O (h)$ bound; it does not exclude a higher order in a particular problem.

[F5]

The real exponential function and the number $e$ by a power series: $e = \sum_{j = 0}^{\infty} 1 / j!$ .

[F6]

$1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ : $1 + x \leq \exp (x)$ for real $x$ .

[F7]

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ : $(1 + x)^{N} = \sum_{j = 0}^{N} (\binom{N}{j}) x^{j}$ for a nonnegative integer $N$ .

[F8]

First-order systems, initial value problems, and solutions on intervals and The exponential function is smooth and $(\exp)^{'} = \exp$ : an exact solution is differentiable, and $\exp^{'} (t) = \exp (t)$ .

[F9]

Chain sum product and composition rules for Banach derivatives and The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ : the product and chain rules hold, and $\exp (s) \exp (t) = \exp (s + t)$ .

[F10]

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)$ : a differentiable function with zero derivative on an interval is constant there.

[F11]

The exponential function is strictly increasing: if $a \leq b$ , then $\exp (a) \leq \exp (b)$ .

[F12]

One-node Gauss data are midpoint data and Finite explicit-left-Euler spectral deferred-correction sweep: for one-node Gauss data, $Q_{11} = 1 / 2$ and $Q_{Δ} = 0$ , so at a start state $u$ the sweep map is $S_{u} (V) = u + (h / 2) V$ and $q = h / 2$ .

[F13]

Contraction and residual error bound for the SDC sweep: if the inner stage map preserves a nonempty closed product ball and $a < 1$ , $q < 1$ , then the collocation branch exists uniquely in that ball.

[F14]

M-node collocation has local defect order M: for $M = 1$ , the exact-path integrand must satisfy a uniform derivative bound $∥ g_{h}^{'} ∥_{\infty} = O (h)$ .

[A1]

Countable Choice, inherited from the one-node Gaussian moment data used in [F2].

Verification

1.1A1F1F5F6F11F12F13giveninductionalgebra

Let the common state tube be $[0, 2 e]$ and take the time-fiber start sets $U_{n} = [1, e]$ ; the field $f (t, y) = y$ is bounded there by $B = 2 e$ and is $1$ -Lipschitz. For every start $u \in U_{n}$ , use the one-stage closed product ball $C_{u} = [0, 2 u]$ , which contains the constant predictor $U^{0} = u$ . By [F12], for $V \in C_{u}$ the inner/outer sweep map is $S_{u} (V) = u + (h / 2) V$ , whose values lie in $[u, u + h u] \subseteq [u, 2 u] \subseteq C_{u}$ when $0 < h \leq 1$ . The contraction constants are $a = 0$ and $q = h / 2 \leq 1 / 2$ , with $q = (1 / 2) h$ . Thus [F13] supplies the unique local collocation branch in $C_{u}$ , uniformly for the start states used in the stability comparison. Now induct on the mesh index. If all earlier checks passed, then $y_{n} = (1 + h)^{n} > 0$ ; for $n h \leq 1$ , [F6] gives $(1 + h)^{n} \leq \exp (n h)$ and [F11] gives $\exp (n h) \leq e$ , so $y_{n} \in U_{n}$ and the stage set hypotheses just verified apply. The first sweep value is $U^{1} = y_{n} + (h / 2) y_{n}$ , with update residual $r_{0} = h ∣ y_{n} ∣ / 2 \leq e h / 2$ . For sufficiently small $h$ , $e h / 2 \leq 1 - h / 2 = (1 - q) t o l$ , so [F1] returns $U^{0}$ after the first check and the endpoint is $y_{n + 1} = (1 + h) y_{n}$ . This closes the induction for every step.

1.2F8F9F10F14algebra

Let $y$ be any exact IVP solution. By [F8]–[F9], $z (t) = \exp (- t) y (t)$ has derivative $z^{'} (t) = - \exp (- t) y (t) + \exp (- t) y^{'} (t) = 0$ . [F10] on each interval $[0, t]$ gives $z (t) = z (0) = 1$ ; the addition formula [F9] then gives $y (t) = \exp (t)$ and in particular $y (1) = e$ . Thus the exact grid states also lie in $U_{n} = [1, e]$ . On a step starting at $t_{n}$ , the exact-path integrand is $g_{h} (s) = e^{t_{n} + h s}$ , so $g_{h}^{'} (s) = h e^{t_{n} + h s}$ and $∥ g_{h}^{'} ∥_{\infty} \leq e h$ for $0 \leq t_{n} + h s \leq 1$ . This verifies the $M = 1$ exact-path derivative premise in [F14].

2.1F2F3F5F7step 1.1step 1.2algebra∎

The computed final value is $(1 + 1 / N)^{N}$ . For $N \geq 2$ , [F7] gives its $j$ th coefficient as $(\binom{N}{j}) N^{- j} = \frac{1}{j!} \prod_{r = 0}^{j - 1} (1 - r / N)$ for $j \leq N$ , which is at most $1 / j!$ ; omitted terms for $j > N$ are positive in [F5]. The $j = 2$ coefficient alone differs from $1 / 2!$ by $1 / (2 N)$ , so $e - (1 + 1 / N)^{N} \geq 1 / (2 N) = h / 2$ . Therefore this accepted finite-tolerance method is not order two; [F3] supplies an $O (h)$ global-error bound for the uncorrected stage, while [F2] gives order two for the fully solved collocation method. More explicitly, step 1.1 gives $y_{n} = (1 + h)^{n} \geq 1$ , hence the accepted first residual obeys $r_{0} = h y_{n} / 2 \geq h / 2$ . The ratio $r_{0} / h^{3} \geq 1 / (2 h^{2}) \to \infty$ , so the accepted residual is not $O (h^{3})$ . This diagnoses failure of that residual target; the independent endpoint lower bound above proves that the accepted method is not order two.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

93 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

Mathew F. Causley and David C. Seal, On the convergence of spectral deferred correction methods, Communications in Applied Mathematics and Computational Science 14 (2019), §3, Theorem 3.1 (standard reference, not scraped)
Ernst Hairer, Syvert P. Nørsett, and Gerhard Wanner, Solving Ordinary Differential Equations I, 2nd ed., Chapter II §II.7 (standard reference, not scraped)