TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

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.

With a Hermitian matrix, Arnoldi collapses to the Lanczos three-term recurrence and a real symmetric tridiagonal projection

Statement

Let $A$ be Hermitian, and run Arnoldi on $(A, b)$ through step $m$ without breakdown. Write

$A Q_{m} = Q_{m + 1} {\overset{ˉ}{H}}_{m}, Q_{m} = [q_{1} \dots q_{m}] .$

Then there exist real numbers $α_{1}, \dots, α_{m}$ and nonnegative real numbers $β_{1}, \dots, β_{m}$ such that

$A q_{j} = β_{j - 1} q_{j - 1} + α_{j} q_{j} + β_{j} q_{j + 1} (1 \leq j \leq m, q_{0} : = 0, β_{0} : = 0) .$

Moreover, $T_{m} : = Q_{m}^{*} A Q_{m}$ is a real symmetric tridiagonal matrix.

Facts & Assumptions

Given: A Hermitian matrix $A$ and an Arnoldi run through step $m$ without breakdown.

[F1]

The Lanczos process is Arnoldi specialized to a Hermitian matrix, with the phase chosen so that the subdiagonal coefficients are real and nonnegative (The Lanczos process as Arnoldi specialized to a Hermitian matrix, with the usual real-subdiagonal phase convention).

[L1]

Arnoldi yields an orthonormal basis and an upper-Hessenberg factorization $A Q_{m} = Q_{m + 1} {\overset{ˉ}{H}}_{m},$ with column relations $A q_{j} = \sum_{i = 1}^{j + 1} h_{i j} q_{i}$ (Before breakdown, Arnoldi produces an orthonormal Krylov basis and a rectangular upper-Hessenberg factorization).

[L2]

An upper-Hessenberg matrix has $h_{i j} = 0$ for $i > j + 1$ , and a real symmetric tridiagonal matrix has zeros whenever $∣ i - j ∣ > 1$ (Upper Hessenberg matrices and real symmetric tridiagonal matrices).

Proof

technique · direct

1.1

Fix $j$ and let $i \leq j - 2$ . By [L1], $A q_{i}$ lies in $span {q_{1}, \dots, q_{i + 1}}$ , which is orthogonal to $q_{j}$ . Since $A$ is Hermitian, $h_{i j} = q_{i}^{*} A q_{j} = (A q_{i})^{*} q_{j} = 0.$ Together with the upper-Hessenberg zero pattern from [L2], this shows that the only possibly nonzero coefficients in column $j$ are $h_{j - 1, j}$ , $h_{j j}$ , and $h_{j + 1, j}$ . Therefore each Arnoldi column relation collapses to a three-term recurrence.

L1L2algebra

2.1

Hermitian symmetry also gives $h_{j, j - 1} = \overline{h_{j - 1, j}}$ . Under the phase convention in [F1], the subdiagonal coefficients $h_{j + 1, j}$ are real and nonnegative; write $β_{j} : = h_{j + 1, j}$ and $α_{j} : = h_{j j}$ . Since $h_{j j} = q_{j}^{*} A q_{j}$ equals its own complex conjugate, each $α_{j}$ is real. Hence $A q_{j} = β_{j - 1} q_{j - 1} + α_{j} q_{j} + β_{j} q_{j + 1},$ which is the Lanczos recurrence.

F1step 1.1algebra

3.1

The projected matrix is $T_{m} = Q_{m}^{*} A Q_{m} = (q_{i}^{*} A q_{j})_{i, j} = (h_{i j})_{1 \leq i, j \leq m}$ . Step 1.1 shows $h_{i j} = 0$ for $∣ i - j ∣ > 1$ , and Hermitian symmetry together with the reality from step 2.1 shows $h_{i j} = h_{j i} \in R$ on the remaining bands. Thus $T_{m}$ is a real symmetric tridiagonal matrix in the sense of [L2].

L2step 1.1step 2.1∎

Depends on

Used by

Cited to discharge well-definedness by The Lanczos process as Arnoldi specialized to a Hermitian matrix, with the usual real-subdiagonal phase convention.

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

Richard Barrett et al., Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods (standard reference, not scraped)