{"id":"palomar/PALOMAR-2026-10-21-000001","url":"https://github.com/zijie123123/PottsDiscontinuity-lean/tree/435fb57856860eda7a65c8fec9e5fb29eff2b46b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000001-v1.json","repo":"https://github.com/zijie123123/PottsDiscontinuity-lean","tags":["math.PR","math-ph","msc:82B20","msc:82B26","msc:82B43","msc:60K35","msc:82B23","statistical-mechanics","potts-model","random-cluster-model"],"score":0,"title":"Discontinuity of the phase transition for the planar random-cluster and Potts models with q > 4 (Theorems 1.1 and 1.2)","trust":"high","domain":"math.PR","source":"palomar","authors":["Zijie Zhuang"],"reviews":0,"subject":"math.PR","summary":"A complete Lean 4 / Mathlib formalization of Theorems 1.1 and 1.2 of Duminil-Copin, Gagnebin, Harel, Manolescu and Tassion (arXiv:1611.09877v2). For the q-state Potts model on the square lattice with q > 4, at beta_c = log(1 + sqrt q), the q + 1 box-limit Gibbs measures are distinct and ergodic, each monochromatic measure gives its own colour probability greater than 1/q at the origin, and the inverse correlation length in the diagonal direction is lambda + 2 sum_{k >= 1} (-1)^k tanh(k lambda) / k, where cosh lambda = sqrt(q) / 2, a positive number. For the random-cluster model on the square…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Discontinuity of the phase transition for the planar random-cluster and Potts models with q > 4","identifier":"arXiv:1611.09877v2","relationship":"formalizes"},{"title":"The Bethe ansatz for the six-vertex and XXZ models: an exposition","identifier":"arXiv:1611.09909v1","relationship":"formalizes"}]}