Read-back: matthews_upper

Let $V$ be a finite, nonempty type (with decidable equality) and let $P$ be a $V \times V$ matrix of real numbers, assumed to be stochastic ($P(x,y) \ge 0$ for all $x,y$, and each row sums to $1$: $\sum_y P(x,y) = 1$ for every $x$) and "irreducible" in the following sense: for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ — the exponent $t = 0$ is allowed, and $P^0$ is the identity, so the case $x = y$ holds trivially. For a length-$t$ vertex sequence $\omega = (\omega_0, \dots, \omega_t)$ let its weight be $\prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$ (the empty product $1$ when $t=0$). Define three quantities by unfolding the custom definitions in the statement. (i) For $x, y \in V$, the "expected hitting time" is $h(x,y) = \sum_{t=0}^{\infty} u_t(x,y)$, where $u_t(x,y)$ is the total weight of all length-$t$ sequences starting at $\omega_0 = x$ that avoid $y$ at every index including index $0$; probabilistically $u_t$ is the chance the walk from $x$ has not visited $y$ through time $t$, so $h(x,y)$ is the expected first-hitting time of $y$ from $x$ — and in the diagonal case $x = y$ every term is $0$ (the start point itself violates avoidance), so $h(x,x) = 0$, not an expected return time. (ii) The quantity written $t_{\mathrm{hit}} = \sup_{(x,y) \in V \times V} h(x,y)$ is the supremum of $h$ over all ordered pairs, diagonal pairs included (harmless, since they contribute $0$). (iii) The "expected cover time from $x$" is $C(x) = \sum_{t=0}^{\infty} r_t(x)$, where $r_t(x)$ is the total weight of all length-$t$ sequences starting at $x$ for which some vertex $y \in V$ is avoided at every index $0, \dots, t$; probabilistically $r_t(x)$ is the chance that the walk from $x$ has not yet visited every vertex by time $t$, so $C(x)$ is the expected time to cover $V$; and $t_{\mathrm{cov}} = \sup_{x \in V} C(x)$. All infinite series here are Lean tsums, which take the value $0$ whenever the series fails to be summable, and the suprema are real-number suprema over finite nonempty index sets (hence genuine maxima). With $n = |V| \ge 1$ the cardinality of $V$, the theorem asserts the single non-strict inequality

i.e. the largest expected cover time over all starting states is at most the largest expected pairwise hitting time multiplied by the harmonic number $H_n = 1 + \tfrac12 + \dots + \tfrac1n$ (here the sum runs over the integers $k$ from $1$ to $n$ inclusive, so $H_1 = 1$ when $V$ has a single element, in which case both $t_{\mathrm{cov}}$ and $t_{\mathrm{hit}}$ are $0$ and the claim is trivially true). No aperiodicity, reversibility, or stationarity assumption appears — only stochasticity and the irreducibility condition above.