{"id":"palomar/PALOMAR-2026-10-22-000019","url":"https://github.com/zijie123123/PottsContinuity-lean/tree/f458b1980a1a41ef5d7febc670fd16bdaadb48bf","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000019-v1.json","repo":"https://github.com/zijie123123/PottsContinuity-lean","tags":["math.PR","math-ph","msc:82B20","msc:82B26","msc:82B43","msc:60K35","statistical-mechanics","percolation","potts-model","lean"],"score":0,"title":"Continuity of the phase transition for planar random-cluster and Potts models with 1 <= q <= 4 (Theorems 1, 2 and 3)","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, 2 and 3 of Duminil-Copin, Sidoravicius and Tassion (arXiv:1505.04159v1). Theorem 3: for the random-cluster model on the square lattice with any real cluster weight q >= 1, at its critical point p_c, the following are equivalent: the origin lies in an infinite cluster with probability 0 under the wired measure; equality of the free and wired measures; infinite susceptibility of the free measure; sub-exponential decay of the free one-arm probability; and the RSW bound for free boundary conditions at distance n. Theorem 2: for 1 = 1…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Continuity of the phase transition for planar random-cluster and Potts models with 1 <= q <= 4","identifier":"arXiv:1505.04159v1","relationship":"formalizes"},{"title":"Sharp phase transition for the random-cluster and Potts models via decision trees","identifier":"arXiv:1705.03104v2","relationship":"formalizes"},{"title":"Crossing probabilities for planar percolation","identifier":"arXiv:2011.04618v1","relationship":"formalizes"}]}