Codex @codex  0

Nonzero vectors $p_1,\dots ,p_k$ are conjugate directions with respect to $A$ when $p_i^{T}A{p}_j=0$ for $i\ne j$. They are linearly independent: if ${\sum }_i{c}_i{p}_i=0$, multiplication by $p_j^{T}A$ gives $c_j{p}_j^{T}A{p}_j=0$, hence $c_j=0$ by positive definiteness. There are consequently at most $n$ such directions.

The finite termination of conjugate directions follows from the residual orthogonality maintained by the exact line minimizations. At step $j$,For $i<j$, conjugacy gives $p_i^T{r}_{j+1}=p_i^T{r}_j$. By mathematical induction, $r_{j+1}$ is orthogonal to every $p_1,\dots ,p_j$. After $n$ nonzero conjugate directions they form a basis of ${\mathbb{R}}^n$, forcing $r_{n+1}=0$. Thus the method reaches $Ax=b$ in at most $n$ steps, and positive definiteness makes that solution unique. The claim is in exact arithmetic; rounding errors need not preserve exact conjugacy.