{"id":"palomar/PALOMAR-2026-10-12-000007","url":"https://github.com/scottnarmstrong/Frohlich-Spencer/tree/e01623b7347c272eac9480f04743f38b8d0df223","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000007-v1.json","repo":"https://github.com/scottnarmstrong/Frohlich-Spencer","tags":["math-ph","math.PR","math.SP","msc:47B80","msc:81T25","msc:82B20","msc:82B26","statistical-mechanics","kosterlitz-thouless","lean-formalization"],"score":0,"title":"Classical theorems of Fröhlich and Spencer: the Kosterlitz–Thouless transition, massless phases of abelian gauge theories, and Anderson localization","trust":"high","domain":"math-ph","source":"palomar","authors":["Scott Armstrong","Amélie Loher"],"reviews":0,"subject":"math-ph","summary":"A Lean 4 / Mathlib formalization of three papers of J. Fröhlich and T. Spencer (Communications in Mathematical Physics, 1981, 1982 and 1983), with the two-dimensional multiscale analysis in the finite-volume form of V. Kharash and R. Peled (2017). For the two-dimensional plane rotator it proves the Kosterlitz–Thouless transition: the two-point function decays exponentially at high temperature, while at low temperature it obeys the power-law lower bound of Theorem C and still tends to zero, so that there is no long-range order. The same multiscale expansion in charge ensembles gives the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"The Kosterlitz–Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas","identifier":"doi:10.1007/BF01208273","relationship":"formalizes"},{"title":"Massless phases and symmetry restoration in Abelian gauge theories and spin systems","identifier":"doi:10.1007/BF01213610","relationship":"formalizes"},{"title":"Absence of diffusion in the Anderson tight binding model for large disorder or low energy","identifier":"doi:10.1007/BF01209475","relationship":"formalizes"},{"title":"The Fröhlich–Spencer Proof of the Berezinskii–Kosterlitz–Thouless Transition","identifier":"arxiv:1711.04720v1","relationship":"adapts"}]}