Proposition 1.14 -- existence of a positive stationary distribution

Let $V$ be an arbitrary nonempty finite type with decidable equality, and let $P$ be a $V \times V$ matrix of real numbers. Assume two hypotheses: (i) $P$ is stochastic in the sense that every entry satisfies $P(x,y) \ge 0$ and every row sums to one, $\sum_y P(x,y) = 1$; and (ii) $P$ is irreducible in the sense that for every ordered pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ — note that $t = 0$ is allowed, and since $P^0$ is the identity matrix, the condition is automatically satisfied when $x = y$, so this hypothesis only constrains pairs with $x \neq y$ and in particular says nothing about returns to a state. The theorem then asserts the existence of a function $\pi : V \to \mathbb{R}$ satisfying three conjuncts simultaneously. First, $\pi$ is stationary for $P$: this means both that $\pi$ is a probability distribution ($\pi(x) \ge 0$ for all $x$, and $\sum_x \pi(x) = 1$) and that the row-vector–matrix product fixes $\pi$, i.e. $\sum_x \pi(x)\,P(x,y) = \pi(y)$ for every $y \in V$. Second, $\pi$ is strictly positive: $\pi(x) > 0$ for every $x \in V$. Third, for every $x \in V$,

where $m(x)$ (written expReturnTime P x in the source) is the following explicitly constructed real number. For each $t \ge 0$, define the avoidance mass

where the sum runs over all sequences $\omega = (\omega_0, \omega_1, \dots, \omega_t) \in V^{t+1}$ such that $\omega_0 = x$ and $\omega_i \neq x$ for every index $1 \le i \le t$ (an empty product for $t = 0$, so $a_0(x) = 1$); probabilistically, $a_t(x)$ is the chance that a chain started at $x$ has not yet returned to $x$ by time $t$. Then $m(x) = \sum_{t=0}^{\infty} a_t(x)$, taken as a topological sum of real numbers — with the convention that if the series fails to converge, this sum is defined to be $0$. By the tail-sum formula, $m(x)$ is (when the series converges) the expected first return time to $x$, so the third conjunct asserts $\pi(x) = 1/m(x)$ for every state, in the multiplied form $\pi(x)\, m(x) = 1$; in particular it forces each $m(x)$ to be finite and nonzero as encoded (a divergent series, giving $m(x)=0$, would make the equation $\pi(x)\cdot 0 = 1$ unsatisfiable). The statement claims mere existence ($\exists$, not unique existence) of such a $\pi$.