Alphabeta Math
CorollaryStatement: 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.

If A is invertible, the exact solution of Ax=b lies in the Krylov space at the grade

Statement

Let A be invertible, let b be a vector, and let ν=ν(A,b). If x∗ is the exact solution of Ax=b, then

x∗∈Kν(A,b).

Facts & Assumptions

Given: An invertible matrix A, a vector b, its grade ν=ν(A,b), and the exact solution x∗=A−1b.

[F1]

The relative minimal polynomial qA,b is monic of degree ν and satisfies qA,b(A)b=0 (The grade of a start vector and its relative minimal polynomial).

[L1]

For every m≥ν, one has Km(A,b)=Kν(A,b) (The dimensions of the Krylov spaces grow by one until the grade and then stabilize).

Proof

technique · direct
1.1givenF1algebra

If b=0, then x∗=0∈K0(A,b)=Kν(A,b). Assume now that b≠0. Write qA,b(z)=a0+a1z+⋯+aν−1zν−1+zν. The constant term a0 is nonzero, because a0=0 would give qA,b(z)=zr(z) and then 0=qA,b(A)b=A r(A)b, so invertibility of A would imply r(A)b=0 with deg⁡r=ν−1, contradicting [F1].

2.1F1L1algebra∎

From qA,b(A)b=0 we obtain a0b+A(a1I+⋯+aν−1Aν−2+Aν−1)b=0. Multiplying by A−1 and dividing by a0 yields x∗=A−1b=−a0−1(a1I+⋯+aν−1Aν−2+Aν−1)b, so x∗∈Kν(A,b). The inclusion is already enough, and [L1] shows it persists in every later Krylov space.

Depends on

Used by

Dependency tree · two levels

7 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