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.

A finite FAS V/W cycle terminates with bounded stated work

Statement

Consider an invocation of Finite-budget recursive nonlinear FAS V/W cycle on levels $0, \dots, J$ , where the base solver uses at most $B_{0} < \infty$ counted operations, every nonlinear smoother update and residual evaluation returns in finite work, and every transfer and correction is a finite-dimensional map evaluation. The invocation terminates with one of its declared statuses. If $W_{j}$ is the maximum counted work of a level- $j$ invocation, then $W_{0} \leq B_{0}, W_{j} \leq C_{j} + γ_{j} W_{j - 1} (1 \leq j \leq J),$ where $C_{j}$ is the finite work of that level's pre-smoothing, residual and transfer evaluations, correction, post-smoothing, and status/diagnostic bookkeeping. This recurrence counts the actual nonlinear smoother, coarse-solve, and returned-diagnostic work; it implies no blanket $O (n_{J})$ estimate.

Facts & Assumptions

Given: A finite hierarchy, finite pre/post sweep counts, $γ_{j} \in {1, 2}$ , a finite base-solver budget, and terminating individual function, transfer, smoother, and correction evaluations.

[F1]

Finite-budget recursive nonlinear FAS V/W cycle: recursion decreases the level, the base solver has budget $B_{0}$ , and a level- $j$ cycle has finite pre/post loops and makes $γ_{j}$ recursive calls.

[A1]

At a level $j > 0$ , assume the claimed termination and work bound for level $j - 1$ .

Proof

technique · induction

1.1givenF1base

At level $0$ , the procedure makes one base-solver call with at most $B_{0}$ update calls. Each residual evaluation and status check terminates by the given operational assumptions, so the base invocation returns a declared status and $W_{0} \leq B_{0}$ .

1.2givenF1A1ihalgebra

A level- $j$ invocation performs its finite pre-smoothing sweeps, one residual and restriction evaluation, and at most $γ_{j}$ calls at level $j - 1$ . By [A1], each such call terminates with work at most $W_{j - 1}$ . Recording each returned status, residual, and nested diagnostic list is finite work included in $C_{j}$ . If any call fails, the algorithm returns immediately; otherwise it performs one finite prolongation/correction and its finite post-smoothing sweeps. Thus every branch terminates and its work is at most $C_{j} + γ_{j} W_{j - 1}$ .

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

Induction from level $0$ through the finite maximum level $J$ proves termination and the displayed recurrence for every invocation. Early failure only shortens the corresponding counted work.

Depends on

Finite-budget recursive nonlinear FAS V/W cycle

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Finite-budget recursive nonlinear FAS V/W cycle.

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)