Lower and Upper Bounds for Glauber Dynamics from Typical States of the Low-Temperature Sherrington–Kirkpatrick Model

We study the heat-bath (Glauber) dynamics of the Sherrington–Kirkpatrick model at zero external field and fixed inverse temperature $\beta>1$. We sample the disorder $J$ and an initial configuration $X_0$ from its Gibbs measure. Let $T^J(X_0)$ be the time at which the transition law, conditional on $J$ and the realized $X_0$, first comes within total-variation distance $1/4$ of equilibrium. In continuous time, with rate one per site, we prove that, for every fixed $\omega\in(0,1/4)$, with probability tending to one, $A_\beta n^{7/30}<\log T^J(X_0)\le n^{1-\omega},$ where $A_\beta>0$ depends only on $\beta$. Corresponding bounds hold for the discrete-time chain. These results strengthen OpenAI’s typical-start lower and upper bounds while following their proof architectures. The lower-bound argument introduces a three-replica comparison with a cubic pressure deficit and uses Aronow and Lopatto’s quantitative mean-bias estimate. The upper-bound argument combines a pathwise information–energy cancellation, concentration estimates on a growing mesh, and optimized exponents. We also complete Lean formalizations of two known results: OpenAI’s fluctuation-scale theorem, giving variance $n^{1/3+o(1)}$ for the log partition function, and its mean-bias consequence of order at least $n^{-5/6-\varepsilon}$ for every fixed $\varepsilon>0$. The formal development proves the positive-Laplace-window input needed for the fluctuation theorem. Five specified result groups are formalized, including the continuous-time dynamics upper bound.