The following describes the scope of the Lean formalization related to the following accompanying paper(s):
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
