Alphabeta Math
TheoremStatement: 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 dimensions of the Krylov spaces grow by one until the grade and then stabilize

Statement

Let ν=ν(A,b) be the grade of b relative to A. Then:

  1. for every integer m with 0m<ν, one has dimKm(A,b)=m;
  2. for every integer mν, one has Km(A,b)=Kν(A,b).

Equivalently, the dimensions increase by one at each step until the grade and then stop changing.

Facts & Assumptions

Given: A square matrix A, a vector b, and its grade ν=ν(A,b).

[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).

Proof

technique · direct
1.1

If 0m<ν and j=0m1cjAjb=0, then the polynomial p(z)=j=0m1cjzj satisfies degp<m<ν and p(A)b=0. By minimality in [F1], this forces p=0, so b,Ab,,Am1b are linearly independent. Therefore dimKm(A,b)=m.

F1L1algebra
2.1

Writing qA,b(z)=a0+a1z++aν1zν1+zν, the relation qA,b(A)b=0 from [F1] shows that AνbKν(A,b). Multiplying the same relation by Ak for each k0 gives Aν+kbKν(A,b) as well. Hence every generator of Km(A,b) for mν already lies in Kν(A,b), so Km(A,b)=Kν(A,b).

F1algebra

Depends on

Used by

Dependency tree · two levels

3 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