# All-temperature pressure of orthogonally invariant Ising spin glasses

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

- [All-temperature pressure for orthogonally invariant Ising spin glasses](../../preprints/All-temperature-pressure-for-orthogonally-invariant-Ising-spin-glasses-September-25-2026/paper.pdf)

## Scope

The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional.

The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Pressure and ground-state limits for invariant Ising models | [InvariantIsing.lean](../ComparatorChallenges/InvariantIsing.lean) |