ExampleConstruction: AI-adaptedVerification: 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.

A Krylov chain can stabilize early when the start vector has a short relative minimal polynomial

Example

Let

$A = (\begin{array}{ccc} 0 & 1 & 0 \\ 0 & 0 & 0 \\ 0 & 0 & 5 \end{array}), b = (\begin{array}{c} 0 \\ 1 \\ 0 \end{array}) .$

Then $A b = e_{1}$ , $A^{2} b = 0$ , and the relative minimal polynomial of $b$ is $q (z) = z^{2}$ . Hence

$K_{1} (A, b) = span {e_{2}}, K_{2} (A, b) = span {e_{2}, e_{1}}, K_{m} (A, b) = K_{2} (A, b) (m \geq 2) .$

So the Krylov chain stabilizes at grade $2$ , strictly before the ambient dimension $3$ .

Facts & Assumptions

Given: The matrix $A$ and vector $b$ displayed above.

[L1]

Krylov dimensions grow one step at a time until the grade and then stabilize (The dimensions of the Krylov spaces grow by one until the grade and then stabilize).

Verification

technique · direct

1.1

Direct multiplication gives $A b = e_{1}$ and $A^{2} b = 0$ . Therefore $q (A) b = 0$ for $q (z) = z^{2}$ , while no nonzero polynomial of degree $< 2$ annihilates $b$ because neither $b$ nor $A b$ is zero. Hence the grade is $ν (A, b) = 2$ .

L1algebra

2.1

The displayed Krylov spaces follow from the vectors $b, A b, A^{2} b$ . Since the grade is $2$ , [L1] predicts exactly the stabilization $K_{m} (A, b) = K_{2} (A, b)$ for $m \geq 2$ , which agrees with the calculation.

L1step 1.1∎

Depends on

The dimensions of the Krylov spaces grow by one until the grade and then stabilize

Used by

Nothing in the library uses this result yet.

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

Yousef Saad, CSCI 8314 Set 13: Krylov subspace methods; Introduction; Krylov subspaces; Gram-Schmidt process (review); The Arnoldi process; FOM and GMRES (standard reference, not scraped)