[proofplan]
We work directly with the eigenvalue equation for $H = I - B^{-1}A$. If $Hw = \lambdaw$ for $w \neq 0$, clearing $B^{-1}$ gives $Aw = (1-\lambda)Bw$. Positive definiteness of $A$ rules out $\lambda = 1$. Taking the Hermitian inner product $\bar{w}^\top(\cdot)w$ expresses $\bar{w}^\top Bw$ and $\bar{w}^\top B^\topw$ in terms of $\bar{w}^\top Aw$ and $\lambda$. Substituting into the quadratic form of $B + B^\top - A$ produces the identity $\bar{w}^\top(B + B^\top - A)w = \bar{w}^\top Aw \cdot \frac{1 - |\lambda|^2}{|1-\lambda|^2}$. Positive definiteness of both $A$ and $B + B^\top - A$ then forces $1 - |\lambda|^2 > 0$, giving $|\lambda| < 1$.
[/proofplan]
[step:Derive the eigenvalue relation $Aw = (1-\lambda)Bw$ and rule out $\lambda = 1$]
Let $\lambda$ be an eigenvalue of $H = I - B^{-1}A$ with eigenvector $w \in \mathbb{C}^n \setminus \{0\}$, so $Hw = \lambdaw$. Then
\begin{align*}
(I - B^{-1}A)w = \lambdaw,
\end{align*}
which gives $B^{-1}Aw = (1 - \lambda)w$, hence
\begin{align*}
Aw = (1-\lambda)Bw.
\end{align*}
We verify that $\lambda \neq 1$: if $\lambda = 1$ then $Aw = 0$, contradicting the positive definiteness of $A$ (since $\bar{w}^\top Aw > 0$ for $w \neq 0$, $A$ cannot annihilate any nonzero vector).
[/step]
[step:Express the quadratic form $\bar{w}^\top(B + B^\top - A)w$ in terms of $|\lambda|$]
Set $\alpha := \bar{w}^\top Aw > 0$ (positive definiteness of $A$). From $Aw = (1-\lambda)Bw$, taking the Hermitian inner product with $w$:
\begin{align*}
\alpha = (1-\lambda)\,\bar{w}^\top Bw, \qquad \text{so} \qquad \bar{w}^\top Bw = \frac{\alpha}{1-\lambda}.
\end{align*}
For the transpose term: since $A$ and $B$ have real entries, $\overline{\bar{w}^\top Bw} = \bar{w}^\top B^\topw$, and $\bar{\alpha} = \alpha$ because $\bar{w}^\top Aw$ is real (as $A$ is real symmetric). Therefore:
\begin{align*}
\bar{w}^\top B^\topw = \frac{\alpha}{1-\bar{\lambda}}.
\end{align*}
Substituting into the quadratic form:
\begin{align*}
\bar{w}^\top(B + B^\top - A)w &= \frac{\alpha}{1-\lambda} + \frac{\alpha}{1-\bar{\lambda}} - \alpha = \alpha\left(\frac{1}{1-\lambda} + \frac{1}{1-\bar{\lambda}} - 1\right).
\end{align*}
Combining over the common denominator $(1-\lambda)(1-\bar{\lambda}) = |1-\lambda|^2$:
\begin{align*}
\frac{(1-\bar{\lambda}) + (1-\lambda) - (1-\lambda)(1-\bar{\lambda})}{|1-\lambda|^2} = \frac{2 - \bar{\lambda} - \lambda - 1 + \bar{\lambda} + \lambda - |\lambda|^2}{|1-\lambda|^2} = \frac{1 - |\lambda|^2}{|1-\lambda|^2}.
\end{align*}
Therefore:
\begin{align*}
\bar{w}^\top(B + B^\top - A)w = \alpha \cdot \frac{1 - |\lambda|^2}{|1-\lambda|^2}.
\end{align*}
[guided]
The strategy is to express everything in terms of the single positive scalar $\alpha = \bar{w}^\top Aw$ and the eigenvalue $\lambda$. The eigenvalue relation provides the substitution $\bar{w}^\top Bw = \frac{\alpha}{1-\lambda}$ that eliminates $B$ from the expression. Even though $B$ may be non-symmetric (so $\bar{w}^\top Bw$ can be complex), the sum $\bar{w}^\top Bw + \bar{w}^\top B^\topw = \frac{\alpha}{1-\lambda} + \frac{\alpha}{1-\bar\lambda}$ is real (as it must be, since $B + B^\top$ is symmetric).
The algebraic identity
\begin{align*}
\frac{1}{1-\lambda} + \frac{1}{1-\bar\lambda} - 1 = \frac{1 - |\lambda|^2}{|1-\lambda|^2}
\end{align*}
is the heart of the proof. It converts the spectral information ($|\lambda|$) into a sign that can be read off from the definiteness of $B + B^\top - A$. The factor $\frac{1-|\lambda|^2}{|1-\lambda|^2}$ is positive iff $|\lambda| < 1$, zero iff $|\lambda| = 1$, and negative iff $|\lambda| > 1$.
[/guided]
[/step]
[step:Apply positive definiteness of $B + B^\top - A$ to conclude $|\lambda| < 1$]
Since $B + B^\top - A$ is symmetric positive definite (by hypothesis) and $w \neq 0$:
\begin{align*}
\bar{w}^\top(B + B^\top - A)w > 0.
\end{align*}
From the identity in the previous step:
\begin{align*}
\alpha \cdot \frac{1 - |\lambda|^2}{|1-\lambda|^2} > 0.
\end{align*}
Since $\alpha > 0$ and $|1-\lambda|^2 > 0$ (as $\lambda \neq 1$):
\begin{align*}
1 - |\lambda|^2 > 0 \implies |\lambda| < 1.
\end{align*}
Since this holds for every eigenvalue $\lambda$ of $H$, we conclude $\rho(H) = \max\{|\lambda| : \lambda \text{ eigenvalue of } H\} < 1$.
[guided]
The positive definiteness hypothesis provides the sign constraint that pins down whether eigenvalues lie inside or outside the unit disc. The identity
\begin{align*}
\bar{w}^\top(B + B^\top - A)w = \bar{w}^\top Aw \cdot \frac{1 - |\lambda|^2}{|1-\lambda|^2}
\end{align*}
links the definiteness of $B + B^\top - A$ (a structural property of the splitting) to the eigenvalue modulus $|\lambda|$ (the convergence rate). Positive definiteness forces the factor $\frac{1-|\lambda|^2}{|1-\lambda|^2}$ to be positive, which gives $|\lambda| < 1$.
The power of the Householder-John theorem is its generality: it applies to *any* splitting $A = B - (B - A)$, not just classical splittings like Jacobi or Gauss-Seidel. The two hypotheses — $A$ SPD and $B + B^\top - A$ SPD — are structural conditions on the splitting that are often easy to verify for specific choices of $B$.
Why does $A$ need to be SPD and not just nonsingular? The quantity $\alpha = \bar{w}^\top Aw$ must be real and positive for the sign argument to work. Symmetry gives reality; positive definiteness gives positivity. Without positive definiteness, $\alpha$ could be negative or zero, and the sign of the product $\alpha \cdot \frac{1-|\lambda|^2}{|1-\lambda|^2}$ would not be determined by $|\lambda|$ alone.
Why must $B$ be nonsingular? If $B$ is singular, then $H = I - B^{-1}A$ is not defined. In practice, $B$ is always chosen to be easily invertible (diagonal for Jacobi, triangular for Gauss-Seidel), so nonsingularity is automatic.
[/guided]
[/step]