Theorem 5:1, eq. (5:3a) — the cg residuals are mutually orthogonal

Proved

ConjGrad.Termination.cg_residuals_orthogonal

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 $r_0, r_1, \dots$ be the residuals produced by the conjugate gradient method (3:1) started at $x_0$ . Then

(r_i, r_j) = 0 \qquad (i \ne j).

Mutual orthogonality of the residuals is what bounds the number of nonzero residuals by the dimension $n$ .

Formalization Note The statement is for all indices. After the method reaches the solution the residuals are $0$ (see the definition of the iteration), so the relation continues to hold trivially.

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter

open Matrix

Formal statement

namespace ConjGrad.Termination

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

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 r_i, r_j\rangle = 0 .

The indices are unbounded: 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 $r_0 = p_0 = 0$ , and the recursion with the zero-quotient convention keeps every $r_i = 0$ , so the claim holds.
Zero quotients. Whenever a residual vanishes, the zero-quotient convention governs the steps that follow it, and the claim is asserted for those steps as well.

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