LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

An exact fine root is fixed by the FAS V/W cycle

Statement

For a level- $j$ invocation of Finite-budget recursive nonlinear FAS V/W cycle, let $u^{*}$ satisfy $F_{j} (u^{*}) = f_{j}$ . Suppose each selected pre/post smoother leaves every exact root fixed, every restriction $I_{j} u^{*}$ lies in $U_{j - 1}$ and is selected as the exact coarse root at its zero-defect target, and the base solver returns any initial exact root unchanged. Then the exact-branch FAS V/W cycle leaves $u^{*}$ fixed. This holds for arbitrary admissible transfer maps $I_{j}, R_{j}, P_{j}$ ; no identity such as $R_{j} = I_{j}$ or $I_{j} P_{j} = I$ is needed.

Facts & Assumptions

Given: A finite hierarchy, an exact fine root, root-fixing smoothers, restrictions of each root in the next-level domain, zero-defect coarse branches selecting those restrictions, and a base solver that preserves an initial exact root.

[F1]

Finite-budget recursive nonlinear FAS V/W cycle: a noncoarsest level restricts the current iterate, forms $g_{H} = F_{H} (I u) + R (f - F_{h} (u))$ , solves the coarse FAS problem, corrects by $u + P (v - I u)$ , and applies finitely many pre/post sweeps; its base solver preserves an initial exact root.

[A1]

For every right-hand side at level $j - 1$ , assume the exact-branch cycle leaves any exact root of that equation unchanged.

Proof

technique · induction on the level

1.1givenF1base

At level $0$ , the input is the exact root $u_{0}^{*}$ and the base solver sees zero residual. Its stated contract in [F1] returns that initial root unchanged. Thus the level- $0$ call fixes its exact root.

1.2givenF1A1ihalgebra

At a noncoarsest level, each pre-smoothing sweep leaves $u^{*}$ unchanged. Thus $f_{j} - F_{j} (u^{*}) = 0$ and the restricted coarse target is $g_{H} = F_{j - 1} (I_{j} u^{*})$ . The hypothesis gives $I_{j} u^{*} \in U_{j - 1}$ and selects it as the exact coarse root. The coarse call starts there, so [A1] makes each of the $γ_{j}$ recursive calls return $I_{j} u^{*}$ ; hence the prolongated difference is zero and every post-smoothing sweep fixes $u^{*}$ .

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

Induction proves the exact-root fixed-point property at every finite level. The calculation used only that the transfers have the stated domains and codomains; no algebraic relation among them was used.

Depends on

Finite-budget recursive nonlinear FAS V/W cycle

Used by

Dependency tree · two levels

2 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)