Section 16.1.3 -- adjacent transpositions lower bound
ProvedMarkovMixing.adjacent_transpositions_lowerThe lazy random adjacent transpositions shuffle of a deck of cards does nothing with probability and otherwise swaps the cards in a uniformly chosen pair of neighbouring positions : the identity carries probability and each of the adjacent transpositions probability . Its stationary distribution is uniform. The mixing time is the first time at which , with the total variation distance.
The theorem (§16.1.3 of Levin–Peres–Wilmer) asserts: for every ,
Order steps are necessary, matching the upper bound up to the logarithm. The obstruction is transport: a single card performs a random walk on the positions that advances only when its own position is selected, so moving it across the deck takes order steps.
import Definitions.Def_mm_shuffle
namespace MarkovMixing
/-- **§16.1.3** (LPW): for the lazy random adjacent transpositions shuffle
on `n` cards, `t_mix ≥ n²(n−1)/16`. -/
theorem adjacent_transpositions_lower (n : ℕ) (hn : 2 ≤ n) :
(n : ℝ) ^ 2 * ((n : ℝ) - 1) / 16 ≤
(tMix (groupWalk (adjacentTranspositionDist n))
(uniformDist (Equiv.Perm (Fin n))) : ℝ) := by
sorry
end MarkovMixing
Read-back
What the Lean code literally says, in plain math · claude-fable-5
For every natural number with (this holds for all such , with no asymptotic threshold),
where the right-hand side is a natural number (cast to a real) defined as follows, and on the left is cast to a real and is real subtraction. The state space is the group of permutations of . A weight function is defined by: if is the identity; otherwise if equals the transposition swapping and for some index with (an adjacent transposition; the second point is written in the code but the guard makes it literally ); and for all other permutations. The transition matrix is the random-walk matrix . The reference distribution is the constant function on (the uniform distribution). The distance between two functions is , the supremum over all finite subsets of the absolute difference of sums (note: no factor ). The worst-case distance to at time is , using row of the -th matrix power. Finally, the mixing quantity is taken at the fixed threshold :
which by the natural-number infimum convention equals if no such exists (in which case the claimed inequality would force , impossible for , so the statement implicitly requires the set to be nonempty with a large infimum). The statement carries no hypothesis that is stochastic or that is stationary for it; the only hypothesis is . The inequality is non-strict and is a lower bound on the mixing quantity.
Confirmed by the mission captain (proposal self-audit).