{"id":"palomar/PALOMAR-2026-10-27-000012","url":"https://github.com/nitromannitol/Dynamic-Dimensional-Reduction/tree/108b7212ce189a1effa009dcda3c8a14bf542ba7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000012-v1.json","repo":"https://github.com/nitromannitol/Dynamic-Dimensional-Reduction","tags":["math.PR","math-ph","msc:82C27","msc:37B15","msc:39A12"],"score":0,"title":"Dynamic dimensional reduction in the Abelian sandpile","trust":"high","domain":"math.PR","source":"palomar","authors":["Ahmed Bou-Rabee"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 formalization of the paper \"Dynamic dimensional reduction in the Abelian sandpile\" by Bou-Rabee (Comm. Math. Phys. 390 (2022); arXiv:2009.05968), in a corrected edition of the arXiv source: dimensional reduction and self-similarity of the parallel toppling odometer (Theorem 1.1), the corresponding statements for the sandpile (Corollary 1.1) and the regularity proposition (Proposition 4.1) proved with them by one joint induction over dimension, side length and time, together with every lemma, corollary and proposition of Sections 2 and 3. The main results are stated as published. The…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Dynamic dimensional reduction in the Abelian sandpile","identifier":"arXiv:2009.05968","relationship":"formalizes"},{"title":"Dynamic dimensional reduction in the Abelian sandpile, corrected edition","identifier":"","relationship":"formalizes"}]}