# Critical SK autocorrelation processes and dynamics across the temperature transition

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase](../../preprints/A-spectral-gap-throughout-the-high-temperature-Sherrington-Kirkpatrick-phase-September-24-2026/main.pdf)
- [Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase](../../preprints/Cutoff-throughout-the-high-temperature-Sherrington-Kirkpatrick-phase-September-24-2026/paper.pdf)
- [Critical slowing down in the Sherrington–Kirkpatrick model](../../preprints/Critical-slowing-down-in-the-Sherrington-Kirkpatrick-model-September-24-2026/paper.pdf)
- [Stretched-exponential barriers for typical SK initial states](../../preprints/Stretched-exponential-barriers-for-typical-SK-initial-states-September-24-2026/paper.pdf)

## Scope

For every fixed inverse temperature $0<\beta<1$, the formalization proves a dimension-independent Poincaré inequality for the zero-field Gaussian Sherrington–Kirkpatrick model with probability tending to one over the disorder. Equivalently, the unscaled single-site heat-bath spectral gap stays bounded away from zero. For dynamics that choose one site uniformly at each discrete step, the spectral gap is at least $1/(Cn)$ with probability tending to one, for a constant $C$ depending on $\beta$.

The formalized supporting result proves ratio cutoff for discrete single-site heat-bath dynamics in the zero-field Gaussian Sherrington–Kirkpatrick model for $0\le\beta<1/2$. For every $0<\varepsilon<1/2$ and $\eta>0$, the probability over the disorder that $t_{\mathrm{mix}}(\varepsilon)/t_{\mathrm{mix}}(1-\varepsilon)>1+\eta$ tends to zero as $n\to\infty$. The denominator is positive for all sufficiently large sizes.

The paper's full range $\beta<1$, explicit cutoff location, and continuous-time conclusion are outside this selected statement.

At criticality in the zero-field Sherrington–Kirkpatrick model, the formalization proves that for every fixed $\varepsilon>0$, the continuous-time mixing time lies between $n^{2/3-\varepsilon}$ and $e^{\varepsilon n}$, and the discrete-time mixing count lies between $n^{5/3-\varepsilon}$ and $e^{\varepsilon n}$, with probability tending to one over the Gaussian disorder. The disorder has independent off-diagonal entries of variance $1/n$. Continuous updates have rate one per site; discrete time counts uniformly chosen single-site update attempts. Mixing is worst-start total variation at threshold $1/4$, with holding allowed.

For deterministic times $t_n=o(n^{2/3})$ or update counts $k_n=o(n^{5/3})$, the Gibbs mass of realized starting states still farther than $1/4$ from equilibrium tends to one in probability. For every deterministic positive sequence $M_n\to\infty$, the covariance operator norm and the linear Rayleigh supremum, using the unscaled heat-bath Dirichlet form, both lie between $n^{2/3}/M_n$ and $M_n n^{2/3}$ with probability tending to one. The covariance result does not give an upper bound for the full inverse spectral gap.

The formalization proves a stretched-exponential mixing obstruction for the zero-field Sherrington–Kirkpatrick model at every fixed inverse temperature $\beta>1$. At time $\exp(n^{1/10000})$, the expected Gibbs mass of initial configurations whose total-variation distance from equilibrium exceeds $1/4$ tends to one. Since this mass lies in $[0,1]$, it also tends to one in probability over the disorder.

The result covers both rate-one-per-site continuous-time heat-bath dynamics and the same stated number of discrete update attempts.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Spectral-gap bound throughout the high-temperature SK phase | [SKHighTemperature.lean](../ComparatorChallenges/SKHighTemperature.lean) |
| Discrete mixing-time ratio cutoff for $\beta<1/2$ | [SKRatio.lean](../ComparatorChallenges/SKRatio.lean) |
| Critical SK mixing bounds | [CriticalSKMixing.lean](../ComparatorChallenges/CriticalSKMixing.lean) |
| Equilibrium starts, covariance, and mixing lower bounds | [CriticalSK.lean](../ComparatorChallenges/CriticalSK.lean) |
| Stretched-exponential barriers from typical equilibrium initial states | [SKBarriers.lean](../ComparatorChallenges/SKBarriers.lean) |