Proposition 2.13 -- irreducibility of a group walk

Let $G$ be a finite group (with decidable equality on its elements), and let $\mu : G \to \mathbb{R}$ be a function satisfying the bundle's IsDist predicate, i.e. $\mu(x) \ge 0$ for every $x \in G$ and $\sum_{x \in G} \mu(x) = 1$. Define the $G \times G$ real matrix $P = \mathrm{groupWalk}(\mu)$ by the bundle's definition

(note the order: the entry from $a$ to $b$ is $\mu$ evaluated at $b a^{-1}$). The theorem asserts the following equivalence: $P$ satisfies the bundle's Irreducible predicate — meaning that for every pair of elements $x, y \in G$ there exists a natural number $t \ge 0$ such that the $(x, y)$ entry of the matrix power $P^t$ is strictly positive, $(P^t)(x,y) > 0$ (the exponent $t$ is allowed to be $0$, in which case $P^0$ is the identity matrix, so for $x = y$ the condition is automatically satisfied by $t = 0$) — if and only if the subgroup of $G$ generated by the support set $\{ g \in G \mid \mu(g) > 0 \}$ is the whole group $G$ (i.e. the subgroup closure of the set of elements where $\mu$ is strictly positive equals the top subgroup $\top$). No aperiodicity, symmetry, or non-degeneracy condition on $\mu$ beyond nonnegativity and summing to $1$ is assumed; the statement is an if-and-only-if, quantified over the fixed but arbitrary finite group $G$ and distribution $\mu$.