Papers With

← All papers
First page of Fluctuation bounds for rotationally invariant first-passage percolation

Fluctuation bounds for rotationally invariant first-passage percolation

Scott Armstrong, Ahmed Bou-Rabee

math.PR Oct 30, 2026 · v1
formalization mathlib probability ai-agents
Read PDF arXiv abstract Code
TL;DR
All results are formalized in Lean 4 with Mathlib, developed with AI agents, in a public repository that also covers the companion lattice paper.
Abstract
We prove that in rotationally invariant first-passage percolation on $\mathbb{R}^d$ with $d\geq2$, the passage time $T_n$ over a distance $n$ satisfies $\mathbb{E}[\exp(|T_n-μn|/n^{\frac{1}{2}(1-\varepsilon)})]\leq C$ for some $\varepsilon>0$, where $μ$ is the time constant. This implies that its variance is at most a constant times $n^{1-\varepsilon}$, the bound that Basu, Sidoravicius and Sly proved in the planar case. As in their work, our argument is an induction on the scale, but in place of their proof that the geodesic is chaotic, we use the averaging argument of Benjamini, Kalai and Schramm together with a logarithmic improvement of the Efron-Stein inequality due to Benaïm and Rossignol.
Problem

In rotationally invariant continuum first-passage percolation on R^d (d>=2), it was open whether passage-time fluctuations are smaller than the classical sqrt(n) scale in all dimensions. Basu, Sidoravicius and Sly had proved such a bound only in the planar case.

Approach

The proof is an induction on the length scale. The authors control passage times between cubes, transverse fluctuations, and continuity in the endpoints. In place of a geodesic-chaos argument, they use the Benjamini-Kalai-Schramm averaging argument with the Benaïm-Rossignol logarithmic improvement of the Efron-Stein inequality to obtain a variance gain. All results are formalized in Lean 4 with Mathlib, in a project developed with the help of AI agents.

Results

The passage time satisfies exponential concentration on the scale n^{(1-ε)/2} for some ε>0, which gives Var[T_n] <= C n^{1-ε}. The Lean repository also formalizes the main theorem of the companion lattice paper and records machine-checked lists of errors and gaps found in the earlier Basu-Sidoravicius-Sly papers.