Proposition 6.1 -- $\tau_{top}$ is a strong stationary time

Proved

MarkovMixing.top_to_random_strong_stationary

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Consider the top-to-random shuffle of a deck of $n\ge2$ cards: at each step the top card is removed and reinserted at a position chosen uniformly at random among the $n$ possibilities. A randomized stopping time for a chain is a rule that, after observing the trajectory up to the present, decides (possibly with randomness) whether to stop now; such a rule is a strong stationary time if it is almost surely finite and the state at the moment of stopping is exactly stationary — here, a uniformly random deck — and independent of the stopping time itself.

The theorem (Proposition 6.1 together with Example 6.7 of Levin–Peres–Wilmer) asserts: for any starting deck, the following rule is a strong stationary time for the top-to-random shuffle — stop one shuffle after the card that was originally at the bottom of the deck first reaches the top. Intuition: each time a card is inserted below the original bottom card, it lands in a uniformly random relative position; by the time the original bottom card surfaces, the cards beneath it form a uniformly random arrangement, and one more insertion randomizes the whole deck.

Preamble

import Definitions.Def_mm_stopping

Formal statement

namespace MarkovMixing

/-- **Proposition 6.1 and Example 6.7** (LPW): for the top-to-random shuffle,
the time `τ_top` — one shuffle after the original bottom card first reaches
the top of the deck — is a strong stationary time: the deck at time `τ_top`
is uniformly distributed and independent of `τ_top`. -/
theorem top_to_random_strong_stationary (n : ℕ) (hn : 2 ≤ n)
    (x : Equiv.Perm (Fin n)) :
    IsStrongStationaryTime (topToRandom n) (uniformDist (Equiv.Perm (Fin n))) x
      (topToRandomRule n) := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 6.1, Proposition 6.1 and Example 6.7, pp. 75-78

Read-back

What the Lean code literally says, in plain math · claude-fable-5

For every natural number $n$ with $n \ge 2$ and every permutation $x$ of the $n$ -element set $\{0,1,\dots,n-1\}$ , the theorem asserts the following. Let $P$ be the "top-to-random" transition matrix on the (finite) set of permutations of $\{0,\dots,n-1\}$ , defined entrywise by

P(\sigma,\tau) \;=\; \frac{\#\{\,j \in \{0,\dots,n-1\} \;:\; \tau = \sigma_j\,\}}{n},

where $\sigma_j$ is the function sending position $i$ to $\sigma(i+1)$ when $i < j$ , to $\sigma(0)$ when $i = j$ , and to $\sigma(i)$ when $i > j$ (the arrangement obtained from $\sigma$ by removing the entry at position $0$ and reinserting it at position $j$ , shifting the intervening entries toward position $0$ ); the count is of those $j$ for which $\tau$ agrees with $\sigma_j$ at every position. Let $u$ be the constant function on permutations with value $1/n!$ (the reciprocal of the cardinality of the permutation group). Let $s$ be the randomized stopping rule that assigns, to each time $t$ and each trajectory $\omega = (\omega_0,\dots,\omega_t)$ of permutations, the stopping probability $s_t(\omega) = 1$ if $t \ge 1$ and $\omega_{t-1}(0) = \omega_0(n-1)$ — i.e. the entry at position $0$ of the state one step before the current time equals the entry at position $n-1$ of the initial state — and $s_t(\omega) = 0$ otherwise; in particular this rule never stops at time $t = 0$ , and its decision at time $t$ inspects the state at time $t-1$ , not the state at time $t$ . Define, for each time $t$ and permutation $y$ , the quantity

\sigma_t(y) \;=\; \sum_{\substack{\omega : \{0,\dots,t\} \to \mathrm{Perm} \\ \omega_0 = x,\ \omega_t = y}} \left(\prod_{i=0}^{t-1} P(\omega_i,\omega_{i+1})\right)\left(\prod_{u=0}^{t-1}\bigl(1 - s_u(\omega_0,\dots,\omega_u)\bigr)\right) s_t(\omega),

the probability of following a path from $x$ to $y$ , not stopping at any time before $t$ , and stopping at time $t$ . The conclusion is the conjunction of three statements: (1) $0 \le s_t(\omega) \le 1$ for every $t$ and every trajectory $\omega$ (immediate here since $s$ takes only the values $0$ and $1$ ); (2) $\sum_{t=0}^{\infty} \sum_{y} \sigma_t(y) = 1$ , where the infinite sum over $t$ is a countable sum that takes the junk value $0$ if the family fails to be summable (so this clause asserts in particular that the family is summable with sum $1$ ); and (3) for every time $t$ and every permutation $y$ ,

\sigma_t(y) \;=\; \Bigl(\sum_{z} \sigma_t(z)\Bigr)\cdot \frac{1}{n!},

i.e. conditional on stopping at time $t$ , the stopped state is exactly proportional to the constant density $1/n!$ (uniform over all $n!$ permutations). Note that the statement does not itself assert that $P$ is a stochastic matrix; $P$ enters only through the path weights above, and the hypothesis $n \ge 2$ rules out the degenerate cases $n = 0$ (where the matrix entries would involve division by $0$ ) and $n = 1$ .

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 6.1 -- τtop\tau_{top}τtop​ is a strong stationary time

Proposition 6.1 -- $\tau_{top}$ is a strong stationary time