Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

In exact arithmetic, CG residuals are mutually orthogonal and the search directions are A-conjugate

Statement

Let A be Hermitian positive definite, and run the conjugate-gradient recurrence in exact arithmetic. For all indices i≠j for which the quantities are defined,

⟨ri,rj⟩=0,pi∗Apj=0.

Thus the residuals are mutually orthogonal and the search directions are A-conjugate.

Facts & Assumptions

Given: A Hermitian positive-definite system Ax=b and an exact-arithmetic CG run.

[F1]

CG uses the recurrence xk+1=xk+αkpk,rk+1=rk−αkApk,pk+1=rk+1+βkpk with αk=⟨rk,rk⟩⟨Apk,pk⟩,βk=⟨rk+1,rk+1⟩⟨rk,rk⟩ (The conjugate-gradient recurrence).

[L1]

If rk≠0, then pk∗Apk>0 (Before convergence, every CG denominator pk∗Apk is positive).

Proof

technique · induction on the later index
1.1F1baseihalgebra

We prove by induction on k≥0 that r0,…,rk are pairwise orthogonal and p0,…,pk are pairwise A-conjugate. For k=0 there is nothing to prove. Assume the claim through step k. Because pj=rj+βj−1pj−1 for j≥1 and rj=pj−βj−1pj−1, the spans span⁡{p0,…,pj} and span⁡{r0,…,rj} agree for every j.

2.1F1L2step 1.1ihalgebra

For i<k, the induction hypothesis and step 1.1 give ⟨ri,rk+1⟩=⟨ri,rk⟩−αk⟨ri,Apk⟩=−αk⟨ri,pk⟩A=0, using [L2], because ri lies in span⁡{p0,…,pi} and pk is A-conjugate to each of those earlier directions. Also, ⟨rk,rk+1⟩=⟨rk,rk⟩−αk⟨rk,pk⟩A. Since rk=pk−βk−1pk−1 for k≥1, the induction hypothesis gives ⟨rk,pk⟩A=⟨pk,pk⟩A, and for k=0 the same identity is immediate. Using [F1], we obtain ⟨rk,rk+1⟩=⟨rk,rk⟩−αk⟨pk,pk⟩A=0. Thus rk+1 is orthogonal to every earlier residual.

3.1F1L1step 2.1discharge-inductionalgebra∎

For i<k, Hermitian symmetry and [F1] give pi∗Apk+1=pi∗Ark+1+βkpi∗Apk=(Api)∗rk+1. Because Api=αi−1(ri−ri+1) from [F1], step 2.1 implies (Api)∗rk+1=0, so pi∗Apk+1=0. For i=k, step 2.1 yields ⟨rk,rk+1⟩=0, hence pk∗Ark+1=(Apk)∗rk+1=αk−1(rk−rk+1)∗rk+1=−αk−1⟨rk+1,rk+1⟩. Therefore pk∗Apk+1=pk∗Ark+1+βkpk∗Apk=−αk−1⟨rk+1,rk+1⟩+βkpk∗Apk=0, because βk=⟨rk+1,rk+1⟩/⟨rk,rk⟩ and αk=⟨rk,rk⟩/(pk∗Apk) by [F1], with positivity from [L1] ensuring these divisions are valid before convergence. This closes the induction.

Depends on

Used by

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources