# QAOA attains the SK optimum in the thermodynamic-first limit

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

- [QAOA attains the SK ground-state energy in the thermodynamic-first limit](../../preprints/QAOA-attains-the-SK-ground-state-energy-in-the-thermodynamic-first-limit-September-25-2026/QAOA-attains-the-SK-ground-state-energy-in-the-thermodynamic-first-limit-September-25-2026.pdf)
- [Full support of the zero-temperature Sherrington–Kirkpatrick order parameter](../../preprints/Full-support-of-the-zero-temperature-Sherrington-Kirkpatrick-order-parameter-September-27-2026/main.pdf)

## Scope

The linked formalization supplies variational identities for the Gaussian zero-field Sherrington–Kirkpatrick ground-state energy used in the paper's QAOA argument. Conditional on an admissible Parisi minimizer and its associated diffusion, it proves convergence of the finite-system ground-state energy, identifies its limit with the Parisi value, and gives equivalent terminal-martingale and integrated-curvature formulas.

It also proves convergence of finite Gaussian coefficient sums to the curvature integral, which approaches the ground-state value as the terminal time tends to one. The selected statement covers these value and approximation results; it does not itself assert convergence of QAOA circuit energies.

The formalization proves that every admissible integrable minimizer of the zero-temperature Parisi functional for the pure zero-field Sherrington–Kirkpatrick model has full relative Stieltjes support on $[0,1)$. Equivalently, the order parameter increases strictly between every two overlap values below one, so its support has no gap. The covariance normalization is $\xi(t)=t^2/2$.

The statement also constructs the associated diffusion and proves its selected self-consistency moment identities. It is conditional on the order parameter being a minimizer and does not separately assert existence of a minimizer.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Parisi ground-state value identities and finite Gaussian approximation | [SKValue.lean](../ComparatorChallenges/SKValue.lean) |
| Full support of zero-temperature SK minimizers | [SKFullSupport.lean](../ComparatorChallenges/SKFullSupport.lean) |