A quantitative replica-symmetric bound for Sherrington–Kirkpatrick model in the entire de Almeida–Thouless region
Seiichiro Kusuoka, Shuta Nakajima
math.PR
Aug 24, 2026 · v2
math-ph
TL;DR
The main overlap concentration, free-energy correction, susceptibility, and overlap CLT theorems are formalized in Lean 4 with Mathlib, with a public repository.
Abstract
We consider the Sherrington–Kirkpatrick model with inverse temperature $β>0$ and deterministic external field $h>0$. Let $q$ be the replica-symmetric fixed point: $q=\mathbb E{\rm tanh}^2 (h+β\sqrt q\,Z)$, where $Z$ is a standard normal. We prove that, uniformly on compact subsets of the strict de Almeida–Thouless region: $β^2\mathbb E{\rm sech}^4(h+β\sqrt{q} Z) <1,$ the overlap satisfies the concentration: $$ \mathbb E\langle (R_{12}-q)^2\rangle=O(N^{-1}). $$ As a consequence, we obtain an $O(N^{-1})$ replica-symmetric free-energy correction and identify the finite-volume replicon susceptibility. Our proof is self-contained and does not use the identification of the limiting free energy with the Parisi variational formula. Moreover, we prove the central limit theorem for the overlap in this region. The present paper provides an alternative proof of the replica-symmetric free energy formula in the de Almeida–Thouless region, which was recently established by Lopatto [arXiv:2604.11921]. An advantage of our approach is that it establishes an explicit quantitative bound and yields the replica-symmetric free energy formula as a consequence. The main result supersedes the corresponding result in our recent preprint arXiv:2607.23427, extending the replica-symmetric bounds to the strict de Almeida-Thouless region. However, we keep the previous preprint, since its argument is different and substantially simpler than the one given here.
Problem
The paper studies the Sherrington–Kirkpatrick spin glass with external field h>0 throughout the strict de Almeida–Thouless region. The goal is to prove quantitative replica-symmetric bounds without relying on the Parisi formula.
Approach
Coercivity estimates for the replica-symmetric solution are derived using tilted heat semigroups. These are combined with preliminary overlap concentration and last-spin cavity approximations, and the cubic remainders are absorbed. A cavity argument then yields a CLT for the overlap. The main theorems are formalized in Lean 4 with Mathlib, with Codex assistance, in the repository njimaMath/research_public/RSAT.
Results
Uniformly on compact subsets of the strict AT region, E⟨(R12−q)^2⟩=O(1/N). The paper also obtains an O(1/N) free-energy correction, the asymptotics of the replicon susceptibility, and a Gaussian CLT for √N(R12−q). These results are machine-checked as strictAT_main and strictAT_overlapCLT_weak.