{"id":"palomar/PALOMAR-2026-11-01-000017","url":"https://github.com/nitromannitol/FPP-variance/tree/cfe58d1d241d86bd831c2e1b3c61273200fb780b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000017-v1.json","repo":"https://github.com/nitromannitol/FPP-variance","tags":["math.PR","msc:60K35","msc:82B43","msc:60K37"],"score":0,"title":"Fluctuation bounds for first-passage percolation","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong","Ahmed Bou-Rabee"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 / Mathlib formalization of two papers of S. Armstrong and A. Bou-Rabee on the fluctuations of passage times in first-passage percolation. \"Curvature and variance in lattice first-passage percolation\": for independent, identically distributed edge weights on Z^d, d >= 2, whose law nu has an exponential moment and nu({0}) below the critical probability of bond percolation (Assumption (W)), and for constants delta in (0, 1], r > 0, Lambda >= 0 and lambda > 0, there are epsilon > 0 and C such that E exp(|T(0, x) - mu(x)| / (C |x|^((1 - epsilon)/2))) = 2, with chi smooth, radial and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Curvature and variance in lattice first-passage percolation","identifier":"","relationship":"formalizes"},{"title":"Fluctuation bounds for rotationally invariant first-passage percolation","identifier":"","relationship":"formalizes"}]}