TheoremStatement: AI-adaptedProof: 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 verified MGRIT error-matrix contraction controls error and residual

Statement

Let $A_{t} u_{*} = b$ be the fine-grid system from The all-at-once bidiagonal time operator and C/F points. By Eliminating F-points gives the exact coarse time operator, $A_{t}$ is invertible. Let $E$ be the exact error matrix for one fixed two-level cycle in A declared two-level MGRIT coarse-correction cycle. Choose a real-valued norm $∥ \cdot ∥$ on $(R^{d})^{N}$ and define its induced operator norm by $∥ T ∥ = \sup_{v \neq 0} ∥ T v ∥ / ∥ v ∥$ . Assume $∥ A_{t} ∥$ and $∥ A_{t}^{- 1} ∥$ are finite for this norm. If a direct calculation or other proof establishes $∥ E ∥ \leq q < 1$ , then after $r \geq 0$ cycles the error satisfies $∥ e^{(r)} ∥ \leq q^{r} ∥ e^{(0)} ∥$ , with the convention $q^{0} = 1$ . The residual $s^{(r)} = b - A_{t} u^{(r)} = A_{t} e^{(r)}$ obeys $∥ s^{(r)} ∥ \leq ∥ A_{t} ∥ q^{r} ∥ e^{(0)} ∥$ , and for every error/residual pair, $∥ s ∥ \leq ∥ A_{t} ∥ ∥ e ∥, ∥ e ∥ \leq ∥ A_{t}^{- 1} ∥ ∥ s ∥ .$

The contraction hypothesis is a property to prove for the declared operators, norm, and cycle. The MGRIT name alone supplies no such bound, and this theorem makes no multilevel convergence claim.

Facts & Assumptions

Given: A finite linear time system, the declared exact two-level cycle and a chosen product-space norm.

[F1]

A declared two-level MGRIT coarse-correction cycle: one cycle has error matrix $E = S_{p o s t} (I - P A_{c}^{- 1} R A_{t}) S_{p r e}$ .

[F2]

Eliminating F-points gives the exact coarse time operator: the fine-grid operator $A_{t}$ is invertible.

[F3]

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms: the chosen vector norm separates zero: $∥ v ∥ = 0$ if and only if $v = 0$ .

[A1]

The directly calculated or proved induced norm satisfies $∥ E ∥ \leq q < 1$ .

[A2]

The induced norms $∥ A_{t} ∥$ and $∥ A_{t}^{- 1} ∥$ are finite for the chosen product-space norm.

Proof

1.1givenF1algebra

By [F1], one cycle sends the current error to $e^{(r + 1)} = E e^{(r)}$ .

2.1givenF3A1step 1.1inductionalgebra

At $r = 0$ the claimed inequality is equality. If the bound holds at $r$ and $e^{(r)} = 0$ , [F3] gives $E e^{(r)} = 0$ and the next bound follows. If $e^{(r)} \neq 0$ , the induced-norm definition in the Statement and [A1] give $∥ e^{(r + 1)} ∥ = ∥ E e^{(r)} ∥ \leq ∥ E ∥ ∥ e^{(r)} ∥ \leq q^{r + 1} ∥ e^{(0)} ∥$ . Induction proves the error bound for every $r \geq 0$ .

3.1givenF2F3A2step 2.1algebra

Since $A_{t} u_{*} = b$ , subtraction gives $s^{(r)} = A_{t} (u_{*} - u^{(r)}) = A_{t} e^{(r)}$ . If $e^{(r)} = 0$ , [F3] gives $s^{(r)} = 0$ . Otherwise the induced-norm definition in the Statement and [A2] give $∥ s^{(r)} ∥ \leq ∥ A_{t} ∥ ∥ e^{(r)} ∥$ , and step 2.1 yields the displayed residual estimate.

4.1givenF2F3A2algebra∎

For any error/residual pair, $s = A_{t} e$ and [F2] gives $e = A_{t}^{- 1} s$ . If $e = 0$ , then $s = 0$ and [F3] gives both inequalities. If $e \neq 0$ , invertibility forces $s \neq 0$ , so the induced-norm definition in the Statement and [A2] give both $∥ s ∥ \leq ∥ A_{t} ∥ ∥ e ∥$ and $∥ e ∥ \leq ∥ A_{t}^{- 1} ∥ ∥ s ∥$ .

Depends on

Used by

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

Dependency tree · two levels

17 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)
Ben S. Southworth, Necessary Conditions and Tight Two-Level Convergence Bounds for Parareal and Multigrid Reduction in Time (standard reference, not scraped)