Papers With

← All papers
First page of Cutoff for the Adjacent Transposition Shuffle on a Cycle

Cutoff for the Adjacent Transposition Shuffle on a Cycle

Colin Defant

math.PR Sep 30, 2026 · v1
formalization mathlib probability
Read PDF arXiv abstract Code
TL;DR
The main cutoff theorem is formally certified in Lean 4 on top of Mathlib, with a challenge file checkable via the Comparator tool.
Abstract
In the adjacent transposition shuffle on a cycle, $n$ distinct cards are placed at the vertices of a cycle, and adjacent cards swap positions according to independent Poisson clocks of rate 1. We prove that this Markov chain exhibits total variation cutoff at time $n^2\log n/(8π^2)$, with a window of order at most $n^2\log\log n$.
Problem

The question is whether the adjacent transposition shuffle on a cycle, where adjacent cards swap at independent rate-1 Poisson clocks, exhibits total variation cutoff, and at what time.

Approach

The authors reveal card positions one at a time in a uniformly random order and use the entropy chain rule to compare each revealed position with one-card transition probabilities. The resulting prediction error is expressed through a reversible two-copy Markov chain. That error is bounded by a uniform local Poincaré inequality combined with a multiscale decomposition. The proofs were produced through human-AI collaboration and certified formally in Lean using Mathlib.

Results

The chain exhibits cutoff at time n^2 log n/(8π^2), with a window of order at most n^2 log log n. A Lean formal certificate of Theorem A relies on no results beyond those already in Mathlib.