Theorem 5.5 -- the lazy walk on the torus mixes in order $n^2$

Fix a natural number $d$ with $d \ge 1$ (the dimension; it is a hypothesis, so $d = 0$ is excluded). The theorem asserts: there exists a real constant $c > 0$ — a single constant that may depend on $d$ but must work uniformly in everything quantified after it — such that for every natural number $n$ that is nonzero (a typeclass hypothesis) and satisfies $n \ge 2$, and for every real $\varepsilon$ with $0 < \varepsilon \le 1/2$, the following inequality holds. The state space is the $d$-dimensional discrete torus: the set of functions $x : \{0,\dots,d-1\} \to \mathbb{Z}/n\mathbb{Z}$ (so $n^d$ states). Its graph structure declares $x \sim y$ exactly when $x \ne y$ and there is a coordinate $j$ with $x_i = y_i$ for all $i \ne j$ and $y_j = x_j + 1$ or $y_j = x_j - 1$ in $\mathbb{Z}/n\mathbb{Z}$ (note that for $n = 2$ the two options coincide, so each vertex has exactly $d$ neighbors rather than $2d$). The simple random walk matrix $W$ on this graph has $W(x,y) = 1/\deg(x)$ when $x \sim y$ and $0$ otherwise, and the chain considered is its lazy version $P = \tfrac12 I + \tfrac12 W$. The target distribution is the uniform distribution $u$ assigning mass $n^{-d}$ to every state. Total-variation distance is defined as $\mathrm{d_{TV}}(\mu,\nu) = \sup_{A} \big|\sum_{x \in A}\mu(x) - \sum_{x \in A}\nu(x)\big|$, the supremum over all subsets $A$ of the state space, and the worst-case distance to $u$ at time $t$ is $d(t) = \sup_x \mathrm{d_{TV}}\big(P^t(x,\cdot),\, u\big)$, where $P^t(x,\cdot)$ is row $x$ of the $t$-th matrix power. The mixing time is

with the convention that the infimum of an empty set of naturals is $0$ — so if no time $t$ ever achieved $d(t) \le \varepsilon$, the left-hand side would be $0$ and the inequality would hold trivially; note also that this definition takes the infimum, not a least element, and does not by itself assert that $d(t) \le \varepsilon$ at the infimum, nor that $d$ is monotone. The asserted inequality is

where the natural number $t_{\mathrm{mix}}(\varepsilon)$ is cast to a real, $n^2$ means the real cast of $n$ squared (the bound grows with $n$ but is independent of the dimension exponent — there is no $d$, $\log n$, or $n^d$ factor on the right beyond what is absorbed into $c$), and $\log_2(\varepsilon^{-1})$ is the base-$2$ logarithm of $1/\varepsilon$, which is $\ge 1$ under the hypothesis $\varepsilon \le 1/2$. Nothing further is asserted: the order of quantifiers is $\forall d,\, \exists c,\, \forall n,\, \forall \varepsilon$, so $c$ may not depend on $n$ or $\varepsilon$, and the claim is only an upper bound ($\le$), with no matching lower bound.