Read-back: cutoff_necessary

Fix, for every natural number $n$: a finite nonempty state space $V_n$ (decidable equality), a real matrix $P_n$ on $V_n$, and a function $\pi_n : V_n \to \mathbb{R}$, subject to the following hypotheses, each quantified over all $n$:

• $P_n$ is stochastic (nonnegative entries, rows summing to $1$);
• $P_n$ is irreducible in the sense that for every ordered pair of states $x, y$ there exists a natural number $t$ (possibly $t = 0$, for which $P_n^0 = I$, so the diagonal pairs are automatically covered) with $(P_n^t)(x,y) > 0$;
• $P_n$ is aperiodic in the sense that for every state $x$, the natural number $\sup\{d \in \mathbb{N} : d \mid t \text{ for every } t \ge 1 \text{ with } (P_n^t)(x,x) > 0\}$ equals $1$; note this "period" is a $\mathbb{N}$-supremum, and if the return-time set is empty the divisor set is all of $\mathbb{N}$, whose unbounded $\mathbb{N}$-supremum is the junk value $0 \ne 1$, so the hypothesis also implicitly rules that case out;
• $\pi_n$ is stationary for $P_n$ (nonnegative, sums to $1$, $\pi_n P_n = \pi_n$ as row vectors);
• detailed balance holds: $\pi_n(x)\,P_n(x,y) = \pi_n(y)\,P_n(y,x)$ for all $x, y$.

Further fix a real constant $C > 0$ and assume, for every $n$, the product-condition

where $t_{\mathrm{mix}}^{(n)}$ is the natural number $\inf\{t : d_n(t) \le 1/4\}$ (with $d_n(t) = \sup_x \sup_{A \subseteq V_n} |\sum_{y \in A}(P_n^t)(x,y) - \sum_{y\in A}\pi_n(y)|$ the worst-case total-variation-type distance, and the $\mathbb{N}$-infimum equal to $0$ if no such $t$ exists), cast to a real, and $t_{\mathrm{rel}}^{(n)} = \bigl(1 - \lambda^\star(P_n)\bigr)^{-1}$ is the "relaxation time", with $\lambda^\star(P_n) = \sup\{|\lambda| : \lambda \in \mathbb{R},\ \lambda \ne 1,\ \exists f \ne 0,\ P_n f = \lambda f\}$ the supremum of absolute values of real eigenvalues of $P_n$ other than $1$ (eigenvalue meaning: some nonzero real vector $f$ on $V_n$ with the matrix acting on column vectors satisfying $P_n f = \lambda f$). Junk conventions apply here: the real supremum of an empty eigenvalue set is $0$, and the inverse is Lean's total inverse, so $\lambda^\star = 1$ gives $t_{\mathrm{rel}} = 0^{-1} = 0$, in which case the bound reads $t_{\mathrm{mix}}^{(n)} \le 0$. Finally assume $t_{\mathrm{mix}}^{(n)} \to \infty$ as $n \to \infty$ (the natural-number sequence tends to the "at top" filter).

Under all of these hypotheses, the conclusion is the negation of the cutoff property: it is not the case that for every real $\varepsilon \in (0,1)$ the ratio $t_{\mathrm{mix}}^{(n)}(\varepsilon)\big/t_{\mathrm{mix}}^{(n)}(1-\varepsilon) \to 1$ as $n \to \infty$, where $t_{\mathrm{mix}}^{(n)}(\varepsilon) = \inf\{t \in \mathbb{N} : d_n(t) \le \varepsilon\}$ (both mixing times cast to reals; total real division, so a zero denominator makes that term of the sequence $0$). Equivalently, there exists some $\varepsilon \in (0,1)$ for which the stated ratio sequence fails to converge to $1$.