TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Linear FAS exactly reduces to a Galerkin correction V/W cycle

Statement

Let $A_{j} \in R^{n_{j} \times n_{j}}$ , $0 \leq j \leq J$ , be a finite SPD Galerkin hierarchy with full-column-rank prolongations $P_{j}$ and $A_{j - 1} = P_{j}^{T} A_{j} P_{j}$ . At each level set $F_{j} (u) = A_{j} u$ , $R_{j} = P_{j}^{T}$ , and use the exact Galerkin coarse operator $F_{j - 1} (v) = A_{j - 1} v$ , matching residual-correction pre/post smoothers, and the same finite sweep and V/W cycle counts in Finite-budget recursive nonlinear FAS V/W cycle and Finite recursive Galerkin V- and W-cycle for an SPD hierarchy. The exact-branch FAS V/W procedure returns exactly the same iterate as the corresponding linear Galerkin correction V/W-cycle. The iterate restriction $I_{j}$ may be any linear map of the stated dimensions.

Facts & Assumptions

Given: The finite SPD Galerkin hierarchy, $R_{j} = P_{j}^{T}$ , matching residual-correction smoothers and cycle counts, exact coarse branches, and exact coarsest solves.

[F1]

Finite-budget recursive nonlinear FAS V/W cycle: a noncoarsest FAS level forms $g_{H} = F_{H} (I_{j} u) + R_{j} (f_{j} - F_{j} (u))$ , recurses from $I_{j} u$ , and corrects by $u + P_{j} (z - I_{j} u)$ .

[F2]

Finite recursive Galerkin V- and W-cycle for an SPD hierarchy: a linear Galerkin level pre-smooths, restricts the residual $r_{j} = f_{j} - A_{j} u$ , starts the coarse correction at $e = 0$ , repeatedly calls the lower cycle with right side $P_{j}^{T} r_{j}$ , prolongs the returned error, and post-smooths by residual correction.

[F3]

The Galerkin coarse correction is an energy-orthogonal projector: for SPD $A_{j}$ and full-column-rank $P_{j}$ , the Galerkin matrix $A_{j - 1} = P_{j}^{T} A_{j} P_{j}$ is SPD and invertible.

[F4]

A linear Galerkin V/W cycle is translation-covariant: the lower linear V/W cycle obeys $Cycle (j - 1, x + a, b + A_{j - 1} a) = a + Cycle (j - 1, x, b)$ .

[A1]

At level $j - 1$ , assume equality of the FAS and correction-cycle outputs for every initial iterate and right side.

Proof

technique · induction on the hierarchy level

1.1givenF1F2F3base

At level $0$ , both procedures use the same exact solve $A_{0}^{- 1} f_{0}$ , so they return the same iterate for every input.

1.2givenF1F2F3A1algebra

At a noncoarsest level $j$ , the fine pre-smoothers agree, so they produce the same current iterate $u$ and residual $r_{j} = f_{j} - A_{j} u$ . Put $u_{H} = I_{j} u$ . The FAS coarse target is $g_{H} = A_{j - 1} u_{H} + P_{j}^{T} r_{j},$ so its residual relative to the starting coarse value $u_{H}$ is exactly $P_{j}^{T} r_{j}$ .

2.1F1F2F4A1ihstep 1.2algebra

Let $e_{t} = z_{t} - u_{H}$ be the current coarse difference after $t$ recursive coarse calls. By [A1], the next FAS coarse call equals the correction-cycle call with initial iterate $z_{t}$ and right side $g_{H}$ . Applying [F4] with $a = u_{H}$ , $x = e_{t}$ , and $b = P_{j}^{T} r_{j}$ gives $Cycle (j - 1, z_{t}, g_{H}) = u_{H} + Cycle (j - 1, e_{t}, P_{j}^{T} r_{j}) .$ Thus each coarse difference update is exactly the error update in [F2], including repeated W-cycle calls.

3.1F1F2F3step 1.1step 1.2step 2.1discharge-induction: step 2.1algebra∎

After the same number of coarse calls, [F1] prolongs the same error correction as [F2]. Their post-smoothers are identical residual-correction updates, so their returned fine iterates agree. The base case and this induction step prove equality at every level.

Depends on

Used by

A one-level linear FAS correction is the Galerkin correction Example

Dependency tree · two levels

11 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

William L. Briggs, Van Emden Henson, and Steve F. McCormick, A Multigrid Tutorial, 2nd ed., Chapter 6 (standard reference, not scraped)
Harald van Brummelen, Basics of Multigrid Methods, SINTEF winter-school lecture notes (standard reference, not scraped)
Van Emden Henson, Multigrid Methods for Nonlinear Problems: An Overview, UCRL-JC-150259 (standard reference, not scraped)