Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 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.

The GMRES residual has the form rm=pm(A)r0 with pm(0)=1 and deg⁡pm≤m

Statement

Let xm be an mth GMRES iterate for Ax=b with initial residual r0=b−Ax0, and let rm=b−Axm. Then there is a polynomial pm such that

rm=pm(A)r0,pm(0)=1,deg⁡pm≤m.

Moreover, among all polynomials p with deg⁡p≤m and p(0)=1, GMRES chooses one minimizing ∥p(A)r0∥2.

Facts & Assumptions

Given: A GMRES iterate xm with residual rm=b−Axm.

[L1]

Every vector in Km(A,r0) has the form q(A)r0 with deg⁡q<m (The Krylov subspace consists exactly of the vectors p(A)b for zero polynomials or polynomials of degree less than m).

[L2]

GMRES minimizes the residual norm over x0+Km(A,r0) (GMRES minimizes the residual norm over the affine Krylov space x0+Km(A,r0)).

Proof

technique · direct
1.1L1constructalgebra

Since xm−x0∈Km(A,r0), [L1] gives a polynomial q with deg⁡q<m and xm=x0+q(A)r0. Therefore rm=b−Axm=r0−Aq(A)r0=pm(A)r0, where pm(z):=1−zq(z). Then pm(0)=1 and deg⁡pm≤m.

2.1L1L2step 1.1∎

Conversely, every polynomial p with deg⁡p≤m and p(0)=1 can be written as p(z)=1−zq(z) with deg⁡q<m. The corresponding vector x=x0+q(A)r0 lies in x0+Km(A,r0) by [L1], and its residual is p(A)r0. Since [L2] makes xm minimize that residual norm over all such x, the polynomial attached in step 1.1 minimizes ∥p(A)r0∥2 among all admissible p.

Depends on

Used by

Dependency tree · two levels

5 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