Theorem 5:1, eq. (5:3c) — $(p_i,r_j)=0$ for $i<j$ and $(p_i,r_j)=|r_i|^2$ for $i\ge j$

Proved

ConjGrad.Termination.cg_direction_residual

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_i$ , $p_i$ be the residuals and directions produced by the conjugate gradient method (3:1) started at $x_0$ . Then

(p_i, r_j) = 0 \quad (i < j), \qquad (p_i, r_j) = |r_i|^2 \quad (i \ge j).

With $j = i$ this gives $(p_i, r_i) = |r_i|^2$ , which is why the cg step length (3:1b) coincides with the cd step length (4:1a).

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

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter

open Matrix

Formal statement

namespace ConjGrad.Termination

/-- Theorem 5:1, eq. (5:3c) (Hestenes–Stiefel 1952, p. 414). For a symmetric positive
definite `A`, the directions and residuals of the cg-method (3:1) satisfy `(pᵢ, rⱼ) = 0`
for `i < j` and `(pᵢ, rⱼ) = |rᵢ|²` for `i ≥ j`. -/
theorem cg_direction_residual {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) :
    (∀ i j, i < j → (cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ j).r = 0) ∧
    (∀ i j, j ≤ i →
      (cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ j).r = (cgIter A k x₀ i).r ⬝ᵥ (cgIter A k x₀ i).r) := 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:3c)

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. The theorem asserts both of the following:

For all $i, j \in \mathbb{N}$ with $i < j$ ,

\langle p_i, r_j\rangle = 0 .

For all $i, j \in \mathbb{N}$ with $j \le i$ ,

\langle p_i, r_j\rangle = \langle r_i, r_i\rangle .

In part 2 the right-hand side is the squared length of $r_i$ , the residual carrying the same index as the direction. It is not the squared length of $r_j$ .

Degenerate cases.

Unbounded indices. Both parts cover all natural-number indices, including those beyond $n$ .
$n = 0$ . Every dot product is $0$ and both parts hold trivially.
$k = A x_0$ . All $r_i$ and $p_i$ are $0$ , and both sides of each equation are $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

Theorem 5:1, eq. (5:3c) — (pi,rj)=0(p_i,r_j)=0(pi​,rj​)=0 for i<ji<ji<j and (pi,rj)=∣ri∣2(p_i,r_j)=|r_i|^2(pi​,rj​)=∣ri​∣2 for i≥ji\ge ji≥j

Theorem 5:1, eq. (5:3c) — $(p_i,r_j)=0$ for $i<j$ and $(p_i,r_j)=|r_i|^2$ for $i\ge j$