Theorem 6:3 — each cg step shortens the error vector, with the exact decrease (6:5)

Proved

ConjGrad.ErrorDecrease.error_vector_decreases

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

conjugate-gradienterror-analysisnumerical-linear-algebrap2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $A$ be a real symmetric positive definite $n\times n$ matrix, let $k\in\mathbb{R}^n$ , and let $h$ be the solution of $Ah=k$ . Run the cg-method (5:1) from an arbitrary starting point $x_0$ , producing estimates $x_i$ , residuals $r_i$ and direction vectors $p_i$ . Write $y_i=h-x_i$ for the error vector of $x_i$ , $f(x)=(h-x,A(h-x))$ for the error function (4:5) and $\mu(z)=(z,Az)/|z|^2$ for the Rayleigh quotient (4:12).

For every index $i$ with $r_i\neq 0$ (that is, every step $x_i\to x_{i+1}$ that the algorithm actually performs), the step reduces the Euclidean length of the error vector, and the reduction is exactly

|y_i|^2 - |y_{i+1}|^2 = \frac{f(x_{i+1}) + f(x_i)}{\mu(p_i)}, \qquad\text{and}\qquad |y_{i+1}| < |y_i| .

This is Theorem 6:3 of Hestenes and Stiefel, whose step from $x_{i-1}$ to $x_i$ is written here with the index shifted by one. The cg-method minimizes the $A$ -weighted error $f$ , not the Euclidean error; the theorem shows that the Euclidean distance $|h-x_i|$ to the solution also decreases strictly at every step, although the residual $|r_i|$ need not. This justifies stopping the algorithm before the final step.

Formalization Note The hypothesis $r_i\neq 0$ says that step $i+1$ takes place (the paper's range $i\le m$ ); it is needed, since after termination both sides of the identity are $0$ and the strict inequality fails. Termination itself ( $x_m=h$ for some $m\le n$ ) is not assumed. The strict decrease is stated for the squared lengths $(y,y)$ , which is equivalent because lengths are nonnegative.

Preamble

import Mathlib
import Definitions.Def_ConjGrad_ErrorDecrease_cgIter
import Definitions.Def_ConjGrad_ErrorDecrease_errorFun
import Definitions.Def_ConjGrad_ErrorDecrease_rayleigh

open Matrix

Formal statement

namespace ConjGrad.ErrorDecrease

theorem error_vector_decreases {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ h : Fin n → ℝ) (hh : A *ᵥ h = k) (i : ℕ) (hr : (cgIter A k x₀ i).r ≠ 0) :
    (h - (cgIter A k x₀ i).x) ⬝ᵥ (h - (cgIter A k x₀ i).x) -
        (h - (cgIter A k x₀ (i + 1)).x) ⬝ᵥ (h - (cgIter A k x₀ (i + 1)).x) =
      (errorFun A h (cgIter A k x₀ (i + 1)).x + errorFun A h (cgIter A k x₀ i).x) /
        rayleigh A (cgIter A k x₀ i).p ∧
    (h - (cgIter A k x₀ (i + 1)).x) ⬝ᵥ (h - (cgIter A k x₀ (i + 1)).x) <
      (h - (cgIter A k x₀ i).x) ⬝ᵥ (h - (cgIter A k x₀ i).x) := by sorry

end ConjGrad.ErrorDecrease

Source

Hestenes & Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6) (1952), p. 416, Theorem 6:3, eq. (6:5)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $n \in \mathbb{N}$ , and let $A$ be an $n \times n$ matrix with real entries, where the rows and columns are indexed by $\{0,\dots,n-1\}$ . The theorem assumes $A$ is positive definite in Mathlib's sense:

$A$ is symmetric, $A^{\top} = A$ ;
$v^{\top} A v > 0$ for every nonzero $v \in \mathbb{R}^n$ .

It also takes three arbitrary vectors $k, x_0, h \in \mathbb{R}^n$ and assumes

A h = k,

so $h$ solves the linear system with right-hand side $k$ . Since $A$ is positive definite and therefore invertible, $h$ is exactly $A^{-1}k$ . The starting vector $x_0$ is not restricted in any way. Finally, the theorem takes an index $i \in \mathbb{N}$ .

The statement uses three definitions from the bundle, $\mathrm{cgIter}$ , $\mathrm{errorFun}$ and $\mathrm{rayleigh}$ . Their Lean code was not given to me, so the only facts below are what this statement itself shows about them:

$\mathrm{cgIter}(A, k, x_0, j)$ is a record indexed by $j \in \mathbb{N}$ , built from $A$ , $k$ and $x_0$ , with at least three vector fields. Write them $x_j$ , $r_j$ and $p_j$ (the fields .x, .r and .p). The names suggest an iterate, a residual and a search direction, but nothing visible here fixes what they are. In particular, it is not visible whether $x_0$ is the given starting vector or whether $r_j$ equals $k - A x_j$ .
$E(y) := \mathrm{errorFun}(A, h, y)$ is a real number that depends on $A$ , $h$ and a vector $y$ . Its formula is not visible.
$R(p) := \mathrm{rayleigh}(A, p)$ is a real number that depends on $A$ and a vector $p$ . Its formula is not visible.

The last hypothesis is that the $r$ -field of the $i$ -th record is nonzero:

r_i \neq 0.

Under all of these hypotheses, the theorem asserts that the following two statements hold together. Here $\|v\|^2 = v \cdot v = \sum_j v_j^2$ is the ordinary Euclidean squared norm, not a norm weighted by $A$ .

An exact identity:

\|h - x_i\|^2 - \|h - x_{i+1}\|^2 \;=\; \frac{E(x_{i+1}) + E(x_i)}{R(p_i)}.

A strict decrease:

\|h - x_{i+1}\|^2 \;<\; \|h - x_i\|^2.

Degenerate cases:

$n = 0$ : $\mathbb{R}^0$ has only the zero vector, so the hypothesis $r_i \neq 0$ can never hold, and the theorem is vacuously true.
Iterations that have already stopped: for any $n$ , the theorem says nothing about an index $i$ with $r_i = 0$ .
Division by zero: division is total, and dividing by $0$ gives $0$ . If $R(p_i) = 0$ , conclusion 1 therefore asserts $\|h - x_i\|^2 = \|h - x_{i+1}\|^2$ . That contradicts conclusion 2, so in that case the theorem amounts to claiming the hypotheses cannot all hold together. Whether $R(p_i)$ can actually be $0$ , or can be negative, depends on the hidden definition of $\mathrm{rayleigh}$ .
What is covered: the statement holds for every $i \ge 0$ , including $i = 0$ , and for every starting vector $x_0$ . Nothing is said about how many iterations are run.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph