The main theorem on finiteness of 2D sandpile avalanches is accompanied by a Lean 4 formalization using Mathlib, with stated literature inputs as assumptions.
Abstract
In the abelian sandpile model on $\mathbb{Z}^d$, a site with at least $2d$ grains topples by sending one grain to each neighbor. In a box $[-N,N]^d$ whose boundary absorbs grains, adding grains at random sites and toppling defines a Markov chain. Athreya and Járai (2004) constructed the stationary state on $\mathbb{Z}^d$ as the limit of its stationary distributions as $N\to\infty$. They asked whether, when a grain is added at the origin of a sandpile in the stationary state, the resulting avalanche of topplings is finite. Járai and Redig (2008) proved that the answer is yes for $d\geq 3$, using the transience of random walk. We prove, using a different method, that avalanches are also finite for $d=2$.
Problem
In the stationary state of the abelian sandpile on Z^2, it was an open question whether the avalanche caused by adding a grain at the origin is almost surely finite. Járai and Redig had settled the case d>=3 using transience of random walk, which fails in two dimensions.
Approach
Avalanches are followed backward through inverse waves, and the burning bijection relates waves to the uniform spanning tree. This bounds the radius tail by the expected reciprocal of an edge count. That count is identified with edges in a random two-colored rooted forest from Wilson's algorithm, and is bounded below at many scales using effective conductance and stochastic comparison. A second-moment bound uses Kenyon–Wilson grove identities. A Lean 4/Mathlib formalization records the correspondence between paper and Lean declarations, with explicitly listed literature inputs.
Figure 1. An avalanche, in light gray, with one of its waves in dark gray. The burning bijection [ Majumdar and Dhar, 1992 ] , applied separately to the wave and to the rest of the box, turns the sandpile left by the wave into two spanning trees, in light and darker blue. Joining them along a red edge makes the wave the set of vertices whose paths to the sink use that edge. The black paths join th
Results
Avalanches in two dimensions are almost surely finite. The radius satisfies μ(ρ>R) ≤ C(log(R+2))^{-a}.
