§2, p. 4 — the eigenvalues of the transition matrix of an irreducible, reversible Markov chain are real

Let $L$ be the transition matrix of a Markov chain on a finite state set $S$ (nonnegative entries, rows summing to $1$), and suppose the chain is irreducible and reversible: there is a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i, j$. Then every eigenvalue of $L$ is real:

The paper quotes this fact from Brémaud (Chapter 6, Section 2.1); it is what makes the eigenvalues of $B_\pi$ explicit in the proof of Lemma B.2.

Formalization Note. The spectrum is taken over $\mathbb{C}$: $\operatorname{Sp}(L)$ is the spectrum of the complexified matrix, and "real" means zero imaginary part. Irreducibility, stationarity and detailed balance are the published mm_basic notions.