TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Finite-precision CG has a recursive-residual gap and an attainable-accuracy bound

Statement

Let $A \in R^{n \times n}$ , $n \geq 1$ , be symmetric positive definite, let $A x_{*} = b$ , and suppose the computed CG process from The conjugate-gradient recurrence completes steps $k = 0, \dots, j - 1$ in the no-range-failure model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add. Assume $n u < 1$ and $2 u < 1$ , and that every nonzero exact product and partial sum in each length- $n$ matrix-vector dot product is normal-range; exact-zero products and sums are permitted. Write the actual stored scalars and vectors as $α_{k}, {\hat{x}}_{k}, {\hat{r}}_{k}, {\hat{p}}_{k}$ , and compute each component of ${\hat{q}}_{k} = fl (A {\hat{p}}_{k})$ by a rounded length- $n$ dot product. Set $δ_{k}^{A} : = {\hat{q}}_{k} - A {\hat{p}}_{k}$ . Compute the updates componentwise as ${\hat{x}}_{k + 1} = fl ({\hat{x}}_{k} + fl (α_{k} {\hat{p}}_{k})), {\hat{r}}_{k + 1} = fl ({\hat{r}}_{k} - fl (α_{k} {\hat{q}}_{k})),$ where the inner products and outer additions/subtractions are rounded operations and $α_{k}$ is the actual stored scalar used by the algorithm. Define the resulting update errors by $δ_{k}^{x} : = {\hat{x}}_{k + 1} - ({\hat{x}}_{k} + α_{k} {\hat{p}}_{k}), δ_{k}^{r} : = {\hat{r}}_{k + 1} - ({\hat{r}}_{k} - α_{k} {\hat{q}}_{k}) .$ For any index $j$ reached by the process, define $g_{j} : = {\hat{r}}_{j} - (b - A {\hat{x}}_{j}), Γ_{j} : = ∥ g_{0} ∥_{2} + \sum_{k < j} (∥ δ_{k}^{r} ∥_{2} + ∥ A ∥_{2} ∥ δ_{k}^{x} ∥_{2} + ∣ α_{k} ∣ ∥ δ_{k}^{A} ∥_{2}) .$ Here $∥ A ∥_{2}$ is the induced Euclidean operator norm. Then $∥ g_{j} ∥_{2} \leq Γ_{j}, ∥ b - A {\hat{x}}_{j} ∥_{2} \leq ∥ {\hat{r}}_{j} ∥_{2} + Γ_{j} .$ If $λ_{\min} > 0$ is the smallest eigenvalue of $A$ , then $∥ x_{*} - {\hat{x}}_{j} ∥_{A} \leq \frac{∥ b - A {\hat{x}}_{j} ∥_{2}}{\sqrt{λ_{\min}}} \leq \frac{∥ {\hat{r}}_{j} ∥_{2} + Γ_{j}}{\sqrt{λ_{\min}}},$ where $∥ e ∥_{A} = \sqrt{e^{T} A e}$ . The explicit operation errors obey $∥ δ_{k}^{A} ∥_{2} \leq γ_{n} {(\sum_{i = 1}^{n} {(\sum_{ℓ = 1}^{n} ∣ A_{i ℓ} ∣ ∣ {\hat{p}}_{k, ℓ} ∣)}^{2})}^{1 / 2},$ and, when $2 u < 1$ , $∥ δ_{k}^{x} ∥_{2} \leq γ_{2} (∥ {\hat{x}}_{k} ∥_{2} + ∣ α_{k} ∣ ∥ {\hat{p}}_{k} ∥_{2}), ∥ δ_{k}^{r} ∥_{2} \leq γ_{2} (∥ {\hat{r}}_{k} ∥_{2} + ∣ α_{k} ∣ ∥ {\hat{q}}_{k} ∥_{2}) .$ No exact-grade termination or monotonicity of the true residual is asserted.

Facts & Assumptions

Given: The real SPD system, a sequence of finite computed CG steps, the actual update errors in the Statement, and the definitions of $Γ_{j}$ and the energy norm.

[F1]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: each real addition and multiplication is rounded with relative error at most $u$ on a successful normal-range operation, exact-zero operations return zero, and for $k u < 1$ , $γ_{k} = k u / (1 - k u)$ .

[F2]

The computed floating-point dot product obeys componentwise and normwise error bounds: when every exact product, rounded product, and intermediate sum is nonzero normal-range, a length- $n$ dot product has absolute error at most $γ_{n} \sum_{ℓ} ∣ x_{ℓ} y_{ℓ} ∣$ .

[F3]

The conjugate-gradient recurrence: CG updates $x$ by adding $α p$ and updates the recursive residual by subtracting $α A p$ .

[F4]

The energy inner product $⟨ u, v ⟩_{A} = ⟨ A u, v ⟩$ and energy norm $∥ u ∥_{A}$ for a Hermitian positive-definite matrix: for real SPD $A$ , $∥ e ∥_{A}^{2} = e^{T} A e$ .

[F5]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: the real symmetric $A$ has an orthonormal eigenbasis; its eigenvalues are positive by positive definiteness.

[F6]

The matrix norm induced by a published vector p-norm: at $p = 2$ , $∥ A ∥_{2}$ is the supremum of $∥ A v ∥_{2}$ over $∥ v ∥_{2} \leq 1$ , hence $∥ A v ∥_{2} \leq ∥ A ∥_{2} ∥ v ∥_{2}$ .

[F7]

If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n: padding a product of at most $n$ relative-error factors with factors $1$ gives deviation at most $γ_{n}$ when $n u < 1$ .

Proof

1.1givenF3algebra

The update equations in the Statement give $\begin{aligned} g_{k + 1} & = {\hat{r}}_{k} - α_{k} (A {\hat{p}}_{k} + δ_{k}^{A}) + δ_{k}^{r} - (b - A ({\hat{x}}_{k} + α_{k} {\hat{p}}_{k} + δ_{k}^{x})) \\ = g_{k} + δ_{k}^{r} - α_{k} δ_{k}^{A} + A δ_{k}^{x} . \end{aligned}$ The $α_{k} A {\hat{p}}_{k}$ terms cancel exactly.

1.2givenF1F2F7algebra

In a row dot product, each exact product and each partial sum is either zero or normal-range by the Statement. At an exact zero, [F1] gives $fl (0) = 0$ , so its relative-error factor is $1$ ; every nonzero operation has a factor $1 + ε$ with $∣ ε ∣ \leq u$ . Unrolling the left-to-right sum gives at most $n$ such factors in the coefficient of each exact product, so [F7] gives an error at most $γ_{n} \sum_{ℓ} ∣ A_{i ℓ} {\hat{p}}_{k, ℓ} ∣$ , the same bound as the narrower dot-product estimate [F2]. Squaring these $n$ rowwise bounds and summing gives the displayed $∥ δ_{k}^{A} ∥_{2}$ bound. For either vector update, each component consists of one rounded product and one rounded addition or subtraction; an exact-zero operation again contributes factor $1$ . Unrolling those two relative errors and applying [F7] with two factors gives the component bound $γ_{2} (∣ v_{i} ∣ + ∣ α ∣ ∣ p_{i} ∣)$ , where $(v, p)$ is $({\hat{x}}_{k}, {\hat{p}}_{k})$ or $({\hat{r}}_{k}, {\hat{q}}_{k})$ . Taking the Euclidean norm and applying the triangle inequality gives the two displayed $γ_{2}$ bounds.

2.1givenstep 1.1F6induction

Taking Euclidean norms in step 1.1 and using [F6] yields $∥ g_{k + 1} ∥_{2} \leq ∥ g_{k} ∥_{2} + ∥ δ_{k}^{r} ∥_{2} + ∣ α_{k} ∣ ∥ δ_{k}^{A} ∥_{2} + ∥ A ∥_{2} ∥ δ_{k}^{x} ∥_{2} .$ Induction from $k = 0$ proves $∥ g_{j} ∥_{2} \leq Γ_{j}$ . Since ${\hat{r}}_{j} = (b - A {\hat{x}}_{j}) + g_{j}$ , the triangle inequality gives the recursive residual bound.

3.1givenF4F5step 2.1algebra∎

Let $e = x_{*} - {\hat{x}}_{j}$ . Then $A e = b - A {\hat{x}}_{j}$ . In the orthonormal eigenbasis of [F5], $∥ e ∥_{A}^{2} = e^{T} A e = \sum_{i} λ_{i} e_{i}^{2} \leq λ_{\min}^{} \sum_{i} λ_{i}^{2} e_{i}^{2} = λ_{\min}^{} ∥ A e ∥_{2}^{2} .$ Thus $∥ e ∥_{A} \leq ∥ b - A {\hat{x}}_{j} ∥_{2} / \sqrt{λ_{\min}}$ ; step 2.1 then proves the claimed bound.

Depends on

Used by

CG's positive-denominator hypothesis fails on an indefinite system while MINRES can start Example

Dependency tree · two levels

21 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

Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., §13.3, printed pp. 276–281 (standard reference, not scraped)
Youcef Saad, Iterative Methods for Sparse Linear Systems, 2nd ed., §6.7, printed pp. 196–201 (standard reference, not scraped)