TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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.

In exact arithmetic, unrestarted GMRES terminates no later than the relative grade

Statement

Let $A$ be invertible, let $x_{0}$ be an initial guess, let $r_{0} = b - A x_{0}$ , and let $ν = ν (A, r_{0})$ . In exact arithmetic, unrestarted GMRES produces a zero residual no later than step $ν$ .

Facts & Assumptions

Given: An invertible matrix $A$ , an initial guess $x_{0}$ , the initial residual $r_{0} = b - A x_{0}$ , and its grade $ν = ν (A, r_{0})$ .

[L1]

The exact correction $A^{- 1} r_{0}$ lies in $K_{ν} (A, r_{0})$ (If $A$ is invertible, the exact solution of $A x = b$ lies in the Krylov space at the grade).

[L2]

GMRES minimizes the residual norm over $x_{0} + K_{ν} (A, r_{0})$ (GMRES minimizes the residual norm over the affine Krylov space $x_{0} + K_{m} (A, r_{0})$ ).

Proof

technique · direct

1.1

Let $x_{*}$ be the exact solution of $A x = b$ . Then $x_{*} - x_{0} = A^{- 1} (b - A x_{0}) = A^{- 1} r_{0}$ , so [L1] gives $x_{*} \in x_{0} + K_{ν} (A, r_{0})$ .

L1algebra

2.1

The exact solution has residual $b - A x_{*} = 0$ . Since $x_{*}$ is an admissible point in the $ν$ th GMRES affine space, [L2] forces the $ν$ th GMRES residual norm to be at most $0$ , hence equal to $0$ . Therefore unrestarted GMRES terminates by step $ν$ .

L2step 1.1∎

Depends on

Used by

Restarted GMRES preserves cyclewise residual minimization but loses the unrestarted finite-termination guarantee Proposition

Dependency tree · two levels

8 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

Lloyd N. Trefethen and David Bau III, Numerical Linear Algebra (standard reference, not scraped)