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

A scalar diffusion mode gives an explicit two-grid MGRIT matrix

Example

Consider the dissipative scalar mode $\dot{y} = - y$ , discretized on four fine steps of length $h = 1 / 4$ by forward Euler, with C-points $0, 2, 4$ . Then the fine-step multiplier is $α = 3 / 4$ . On each two-step macro interval, use backward Euler with length $H = 1 / 2$ , giving coarse multiplier $ψ = 2 / 3$ . For the two-level cycle in A declared two-level MGRIT coarse-correction cycle with ideal interpolation/restriction and F-relaxation both before and after coarse correction, the error matrix in the node ordering $(u_{1}, u_{2}, u_{3}, u_{4})$ is $E = (\begin{array}{cccc} 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 0 & - \frac{5}{48} & 0 & 0 \end{array}) .$ Its induced $ℓ^{\infty}$ norm is $5 / 48 < 1$ , so this specified cycle contracts. The calculation is for this scalar mode and cycle only; it implies no mesh-independent MGRIT rate.

Facts & Assumptions

Given: The four-step scalar fine recurrence, the two-step coarse propagator, and the stated F-relaxation cycle.

[F1]

The explicit Euler, midpoint, and classical fourth-order Runge–Kutta tableaus: Forward Euler has $s = 1$ , $A = (0)$ , $b = (1)$ , and $c = (0)$ .

[F2]

Backward Euler step equation and algebraic residual: a backward-Euler endpoint satisfies $z = x + h f (t + h, z)$ .

[F3]

The all-at-once bidiagonal time operator and C/F points: $(A_{t} v)_{1} = v_{1}$ and $(A_{t} v)_{i} = v_{i} - Φ_{i} v_{i - 1}$ for later time indices.

[F4]

Eliminating F-points gives the exact coarse time operator: the exact eliminated coarse operator has Schur complement $S = A_{C C} - A_{C F} A_{F F}^{- 1} A_{F C}$ .

[F5]

A declared two-level MGRIT coarse-correction cycle: $P = [\begin{array}{c} - A_{F F}^{- 1} A_{F C} \\ I_{C} \end{array}]$ , $R = [\begin{array}{cc} - A_{C F} A_{F F}^{- 1} & I_{C} \end{array}]$ , and the cycle uses F-relaxation and the corresponding coarse correction.

[F6]

A verified MGRIT error-matrix contraction controls error and residual: if $∥ A_{t} ∥$ and $∥ A_{t}^{- 1} ∥$ are finite and $∥ E ∥ \leq q < 1$ , then the error after $r$ cycles is at most $q^{r} ∥ e^{(0)} ∥$ , with $q^{0} = 1$ .

[F7]

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms: a norm satisfies separation, absolute homogeneity, and the triangle inequality.

[A1]

The fine grid has four steps, coarsening factor $m = 2$ , $h = 1 / 4$ , and the product-space norm is $∥ e ∥_{\infty} = \max_{1 \leq i \leq 4} ∣ e_{i} ∣$ .

Verification

1.1givenF1F2A1algebra

By [F1], each fine Euler step for $\dot{y} = - y$ multiplies by $α = 1 - h = 3 / 4$ . By [F2], a backward-Euler macro step solves $z = x - \frac{1}{2} z$ , so its multiplier is $ψ = 2 / 3$ .

2.1givenF3F4step 1.1algebra

In fine order the error operator is $A_{t} = (\begin{array}{cccc} 1 & 0 & 0 & 0 \\ - α & 1 & 0 & 0 \\ 0 & - α & 1 & 0 \\ 0 & 0 & - α & 1 \end{array})$ . In F/C order $F = (1, 3)$ , $C = (2, 4)$ , its blocks are $A_{F F} = I$ , $A_{F C} = (\begin{array}{cc} 0 & 0 \\ - α & 0 \end{array})$ , $A_{C F} = (\begin{array}{cc} - α & 0 \\ 0 & - α \end{array})$ , and $A_{C C} = I$ . Hence [F4] gives $S = (\begin{array}{cc} 1 & 0 \\ - α^{2} & 1 \end{array})$ .

3.1givenF5step 2.1algebra

F-relaxation maps an error $(e_{1}, e_{2}, e_{3}, e_{4})$ to $(0, e_{2}, α e_{2}, e_{4})$ , so the F-row residuals vanish and the ideal restriction in [F5] reduces to the C residual $(e_{2}, e_{4} - α^{2} e_{2})$ . Solving the practical coarse system $(\begin{array}{cc} 1 & 0 \\ - ψ & 1 \end{array}) z = (e_{2}, e_{4} - α^{2} e_{2})$ gives $z_{1} = e_{2}$ , $z_{2} = e_{4} + (ψ - α^{2}) e_{2}$ . Subtracting the ideal interpolation [F5] leaves $(0, 0, 0, (α^{2} - ψ) e_{2})$ ; post-F-relaxation leaves this vector unchanged.

4.1givenA1step 3.1algebra

Therefore $E$ has its only nonzero entry in row $4$ , column $2$ , equal to $α^{2} - ψ = \frac{9}{16} - \frac{2}{3} = - \frac{5}{48}$ . For the norm in [A1], $∥ E e ∥_{\infty} = \frac{5}{48} ∣ e_{2} ∣ \leq \frac{5}{48} ∥ e ∥_{\infty}$ , with equality when $e = (0, 1, 0, 0)$ . Thus $∥ E ∥_{\infty} = 5 / 48 < 1$ .

5.1givenA1F6F7step 1.1step 2.1step 4.1algebra∎

For every $e \in R^{4}$ , $∥ e ∥_{\infty} = \max_{i} ∣ e_{i} ∣$ is nonnegative and vanishes only when every coordinate is zero; $∥ λ e ∥_{\infty} = ∣ λ ∣ ∥ e ∥_{\infty}$ ; and $∥ e + f ∥_{\infty} \leq ∥ e ∥_{\infty} + ∥ f ∥_{\infty}$ . Thus the norm in [A1] satisfies [F7]. For any matrix $B$ , $∥ B v ∥_{\infty} \leq (\max_{i} \sum_{j} ∣ B_{i j} ∣) ∥ v ∥_{\infty}$ by applying the finite triangle inequality to each row. The row sums of $A_{t}$ are at most $1 + α = 7 / 4$ . If $A_{t} u = w$ , forward substitution gives $u_{1} = w_{1}$ and $u_{i} = w_{i} + α u_{i - 1}$ , hence by induction $u_{i} = \sum_{j = 1}^{i} α^{i - j} w_{j}$ . Therefore $A_{t}^{- 1}$ has entries $α^{i - j}$ for $i \geq j$ and zero otherwise, with row sums at most $1 + α + α^{2} + α^{3} = 175 / 64$ . Thus $∥ A_{t} ∥_{\infty} \leq 7 / 4$ and $∥ A_{t}^{- 1} ∥_{\infty} \leq 175 / 64$ . All hypotheses of [F6] hold with $q = 5 / 48$ , so the error after $r$ cycles is at most $(5 / 48)^{r}$ times its initial value.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

R. D. Falgout, S. Friedhoff, Tz. V. Kolev, S. P. MacLachlan, and J. B. Schroder, Parallel Time Integration with Multigrid (standard reference, not scraped)
V. A. Dobrev, Tz. Kolev, N. A. Petersson, and J. B. Schroder, Two-Level Convergence Theory for Multigrid Reduction in Time (standard reference, not scraped)
Martin J. Gander, Time Parallel Time Integration, Chapter 4: Space-Time Multigrid Methods (standard reference, not scraped)