← All papers
First page of Proof of the Lyons–White Conjecture

Proof of the Lyons–White Conjecture

Colin Defant, Ken Ono

math.PR Aug 27, 2026 · v1
Theorems on rate-monotonicity of random walks on dihedral-type groups were formally verified in Lean using the AxiomProver system.
Let $D_n$ be the dihedral group of order $2n$. Consider a continuous-time random walk on $D_n$ driven by arbitrary symmetric rates whose support generates $D_n$. For $p\in[1,\infty]$, we say the pair $(D_n,p)$ is rate-monotonic if for each fixed time $t$, the $\ell^p$-distance between the random walk's distribution at time $t$ and the uniform distribution is monotonically decreasing as a function of the rates. Lyons and White proved that $(D_n,2)$ and $(D_n,\infty)$ are rate-monotonic. Somewhat counterintuitively, they found several pairs $(D_n,p)$ with ${p\in[1,1.997]\cup[2.001,3.999]\cup[4.001,5.995]}$ that are not rate-monotonic, and they asked whether any such pairs exist with $p=4$ or $p=6$. We resolve their question, proving that $(D_n,2m)$ is rate-monotonic for all positive integers $m$ and $n$. In fact, we prove a generalization of this result to a broader family of groups that includes generalized dihedral groups, dicyclic groups, and generalized quaternion groups. In the other direction, we prove that for every real $p\geq 1$ that is not an even integer, there exists a positive integer $n$ such that $(D_n,p)$ is not rate-monotonic. The results of this paper were formally verified in Lean by AxiomProver assuming standard literature.

For a continuous-time random walk on the dihedral group D_n driven by symmetric rates, the pair (D_n,p) is rate-monotonic if the ell^p-distance to the uniform distribution decreases as rates increase. Lyons and White asked whether (D_n,p) can fail to be rate-monotonic for p=4 or p=6.

The random walk is analyzed via the group algebra, using the centered heat element and spectral/fractional-power techniques on inversion extensions of finite abelian groups, which include dihedral, generalized dihedral, dicyclic, and generalized quaternion groups. For non-even p, integral identities and Riemann-sum arguments produce counterexamples. The main theorems were developed with the AxiomProver AI system and formally verified in Lean, assuming standard analysis and group theory facts.

For all positive integers m and n, (D_n,2m) is rate-monotonic, resolving the p=4 and p=6 questions affirmatively and generalizing to a broader family of groups. Conversely, for every real p>=1 that is not an even integer, some n makes (D_n,p) not rate-monotonic. A Lean certificate for the three theorems is provided.