Theorems 4:2 and 5:2 — the cg-method reaches the solution $h$ in at most $n$ steps

Proved

ConjGrad.ErrorDecrease.cg_terminates

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

conjugate-gradientfinite-terminationnumerical-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$ . Let $x_0,x_1,x_2,\dots$ be the estimates produced by the cg-method (5:1) from an arbitrary starting point $x_0$ . Then there is an index $m$ with

m\le n \quad\text{and}\quad x_m = h .

This is Theorem 4:2 ("The cd-method is an $m$ -step method ( $m\le n$ ) in the sense that at the $m$ th step the estimate $x_m$ is the desired solution $h$ "), applied to the cg-method through Theorem 5:2 ("The cg-method is a cd-method"). It is the setting of Section 6 of the paper, "Let now $x_0,x_1,\dots,x_m=h$ be the estimates of $h$ obtained by applying the cg-method", and it is used in the proof of Theorem 6:3.

Formalization Note The cg sequence is the unguarded recursion of the definition, so after step $m$ it stays at $h$ . Symmetry of $A$ is part of Mathlib's Matrix.PosDef.

Preamble

import Mathlib
import Definitions.Def_ConjGrad_ErrorDecrease_cgIter

open Matrix

Formal statement

namespace ConjGrad.ErrorDecrease

theorem cg_terminates {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ h : Fin n → ℝ) (hh : A *ᵥ h = k) :
    ∃ m ≤ n, (cgIter A k x₀ m).x = h := 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. 412, Theorem 4:2, applied through p. 415, Theorem 5:2; setting of Section 6, p. 416

Read-back

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

Setting and hypotheses.

$n$ is a natural number.
$A$ is a real $n\times n$ matrix that is positive definite: it is symmetric and $z\cdot Az > 0$ for every nonzero $z\in\mathbb{R}^n$ .
$k, x_0 \in \mathbb{R}^n$ are arbitrary vectors.
$h\in\mathbb{R}^n$ satisfies $Ah = k$ .

The sequence. $(x_i, r_i, p_i)_{i\in\mathbb{N}}$ is generated from $A$ , $k$ and $x_0$ as follows:

Start with $x_0$ and $r_0 = p_0 = k - Ax_0$ .
Set $a_i = (r_i\cdot r_i)/(p_i\cdot Ap_i)$ , then $x_{i+1} = x_i + a_i p_i$ and $r_{i+1} = r_i - a_i Ap_i$ .
Set $b_i = (r_{i+1}\cdot r_{i+1})/(r_i\cdot r_i)$ and $p_{i+1} = r_{i+1} + b_i p_i$ .
Any division by zero yields $0$ .

Conclusion. There exists a natural number $m$ with

m \le n \quad\text{and}\quad x_m = h .

The statement only asserts that the solution is hit at some step $m \le n$ . It says nothing about the iterates after step $m$ . It also does not say that $m$ is the first index with $x_m = h$ .

Degenerate cases.

$n = 0$ : the only possible $m$ is $0$ , and $x_0 = h$ holds trivially because all vectors are empty.
$x_0 = h$ : then $m = 0$ works.
Division-by-zero convention: this governs the sequence once a residual vanishes, as described in the definition of the sequence.

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

Theorems 4:2 and 5:2 — the cg-method reaches the solution hhh in at most nnn steps

Theorems 4:2 and 5:2 — the cg-method reaches the solution $h$ in at most $n$ steps