{"id":"palomar/PALOMAR-2026-10-21-000025","url":"https://github.com/pmaronow/fluctuations-palomar/tree/52e8a21a2497f28811a3154dea6d37e819ccc088","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000025-v1.json","repo":"https://github.com/pmaronow/fluctuations-palomar","tags":["math.PR","math.LO","msc:60K35","msc:82B44","msc:03B35","statistical-physics","spin-glasses","mixing-times","lean"],"score":0,"title":"Lower and Upper Bounds for Glauber Dynamics from Typical States of the Low-Temperature Sherrington–Kirkpatrick Model","trust":"high","domain":"math.PR","source":"palomar","authors":["P. M. Aronow"],"reviews":0,"subject":"math.PR","summary":"Lean formalization of five manuscript result groups: Theorems 1.1, 1.3, and 1.6, and Corollaries 1.2 and 1.7. The barrier covers both clocks and every fixed threshold below one half, with exponent 7/30. The upper bound is the continuous-time statement for every fixed exponent saving between zero and one quarter. The fluctuation exponents and mean-bias lower bound have their stated positive exponent slack. Corollary 1.7 also explicitly concludes convergence of the finite-volume counting pressures to the limiting pressure. The manuscript and exact scope are included.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Lower and Upper Bounds for Glauber Dynamics from Typical States of the Low-Temperature Sherrington–Kirkpatrick Model","identifier":"","relationship":"formalizes"},{"title":"Stretched-exponential barriers for typical SK initial states","identifier":"https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb","relationship":"adapts"},{"title":"A typical-start upper bound for low-temperature SK Glauber dynamics","identifier":"https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb","relationship":"adapts"},{"title":"The low-temperature Sherrington–Kirkpatrick fluctuation scale","identifier":"https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb","relationship":"formalizes"}]}