Proof of the Lyons–White Conjecture
Colin Defant, Ken Ono
math.PR
Aug 27, 2026 · v1
TL;DR
Theorems on rate-monotonicity of random walks on dihedral-type groups were formally verified in Lean using the AxiomProver system.
Abstract
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.
Problem
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.
Approach
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.
Results
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.