Theorem 5:1, eq. (5:3b) — the cg directions are mutually conjugate

Proved

ConjGrad.Termination.cg_directions_conjugate

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

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

Let $A$ be a real symmetric positive definite $n \times n$ matrix, let $k, x_0 \in \mathbb{R}^n$ , and let $p_0, p_1, \dots$ be the direction vectors produced by the conjugate gradient method (3:1) started at $x_0$ . Then

(p_i, Ap_j) = 0 \qquad (i \ne j).

This is the relation that makes the cg-method a method of conjugate directions.

Formalization Note The statement is for all indices; after the method reaches the solution the directions are $0$ .

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter

open Matrix

Formal statement

namespace ConjGrad.Termination

/-- Theorem 5:1, eq. (5:3b) (Hestenes–Stiefel 1952, p. 414). For a symmetric positive
definite `A`, the directions `p₀, p₁, …` of the cg-method (3:1) are mutually conjugate:
`(pᵢ, Apⱼ) = 0` for `i ≠ j`. -/
theorem cg_directions_conjugate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) :
    ∀ i j, i ≠ j → (cgIter A k x₀ i).p ⬝ᵥ (A *ᵥ (cgIter A k x₀ j).p) = 0 := 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. 414, Theorem 5:1, eq. (5:3b)

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.

Conclusion. For all $i, j \in \mathbb{N}$ with $i \ne j$ ,

\langle p_i, A p_j\rangle = 0 .

The claim covers all pairs of distinct natural numbers, including indices greater than $n$ .

Degenerate cases.

$n = 0$ . All vectors are empty and the claim holds trivially.
$k = A x_0$ . Then $p_0 = 0$ , and every later $p_i$ is $0$ under the zero-quotient convention, so the claim holds.
Zero quotients. After any residual vanishes, the directions produced by the zero-quotient convention are included in the claim.

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