Theorem 5:2, first sentence — the cg-method is a cd-method

Proved

ConjGrad.Termination.cg_isCDRun

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

conjugate-directionsconjugate-gradientnumerical-linear-algebrap2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $A$ be a real symmetric positive definite $n \times n$ matrix and let $k, x_0 \in \mathbb{R}^n$ . The estimates $x_i$ , residuals $r_i$ and directions $p_i$ produced by the conjugate gradient method (3:1) started at $x_0$ form a run of the method of conjugate directions for $Ax = k$ : for all $i \ge 0$ ,

$r_i = k - Ax_i$ ;
$x_{i+1} = x_i + a_i p_i$ with $a_i = \dfrac{(p_i, r_i)}{(p_i, Ap_i)}$ ;
$(p_{i+1}, Ap_j) = 0$ for $j = 0, 1, \dots, i$ .

In the paper's words: the cg-method is a cd-method. Together with Theorem 4:2 this yields the finite termination of the cg-method.

Formalization Note Only the first sentence of Theorem 5:2 is formalized. The second sentence (the $p_i$ are obtained by $A$ -orthogonalization of the residuals) and the converse ("a cd-method in which the residuals are mutually orthogonal is essentially a cg-method", which the paper qualifies by an informal continuity assumption) are not part of this statement.

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter
import Definitions.Def_ConjGrad_Termination_IsCDRun

open Matrix

Formal statement

namespace ConjGrad.Termination

/-- Theorem 5:2, first sentence (Hestenes–Stiefel 1952, p. 415): the cg-method is a
cd-method. For a symmetric positive definite `A`, the estimates, residuals and directions
produced by the cg-method (3:1) form a run of the cd-method (4:1)–(4:2): `rᵢ = k − Axᵢ`,
`xᵢ₊₁ = xᵢ + ((pᵢ,rᵢ)/(pᵢ,Apᵢ)) pᵢ`, and each `pᵢ₊₁` is conjugate to `p₀, …, pᵢ`. -/
theorem cg_isCDRun {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) :
    IsCDRun A k (fun i => (cgIter A k x₀ i).x) (fun i => (cgIter A k x₀ i).r)
      (fun i => (cgIter A k x₀ i).p) := by sorry

end ConjGrad.Termination

Source

Hestenes & Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6) (1952), https://doi.org/10.6028/jres.049.044, p. 415, Theorem 5:2, first sentence

Read-back

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

Setting. Let $n \in \mathbb{N}$ and let $A$ be a real $n\times n$ matrix that is positive definite in this sense:

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

Here $\langle u,v\rangle = \sum_l u_l v_l$ . Let $k, x_0 \in \mathbb{R}^n$ be arbitrary.

The iteration. Let $(x_i, r_i, p_i)_{i \in \mathbb{N}}$ be the sequence defined recursively as follows. Start with

r_0 = p_0 = k - A x_0 .

Then, for every $i \ge 0$ ,

a_i = \frac{\langle r_i, r_i\rangle}{\langle p_i, A p_i\rangle}, \quad x_{i+1} = x_i + a_i p_i, \quad r_{i+1} = r_i - a_i A p_i,

b_i = \frac{\langle r_{i+1}, r_{i+1}\rangle}{\langle r_i, r_i\rangle}, \quad p_{i+1} = r_{i+1} + b_i p_i .

Every quotient with a zero denominator is $0$ , and the recursion never stops. Only $r_0$ is defined as $k - A x_0$ ; later residuals come from the recursive update.

Conclusion. The three sequences satisfy all of the following:

For every $i \in \mathbb{N}$ ,

r_i = k - A x_i .

For every $i \in \mathbb{N}$ ,

x_{i+1} = x_i + \frac{\langle p_i, r_i\rangle}{\langle p_i, A p_i\rangle}\, p_i ,

with the quotient read as $0$ when $\langle p_i, A p_i\rangle = 0$ . 3. For every $i \in \mathbb{N}$ and every $j \le i$ ,

\langle p_{i+1}, A p_j\rangle = 0 .

Degenerate cases.

Unbounded indices. All indices range over all natural numbers, including those beyond $n$ .
$n = 0$ . Every vector is empty and all three conditions hold trivially.
$k = A x_0$ . Then $r_i = p_i = 0$ and $x_i = x_0$ for all $i$ , so conditions 2 and 3 read $x_{i+1} = x_i$ and $0 = 0$ .

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