\section*{Use of AI}
The statements, proofs, code, Lean formalization and text of this paper were generated mainly by AI systems: Claude Opus 5.5 (Anthropic) derived the proofs and wrote the rest, and GPT-6.1 Sol (OpenAI) wrote an independent report on each result. A final audit by fresh AI readers covered the longer version in the repository, and the certified computations were rebuilt from a clean start.

\section*{Code and data}
The code, the certificates of Section~\ref{sec:digits}, the longer version and the dependencies between the results are at \url{https://github.com/OctopusTide/hopfield-capacity}. The repository also contains a Lean~4 proof of Theorem~\ref{thm:main}(a),(b), Theorem~\ref{thm:main-free-energy}(a),(b), and the statements in Theorem~\ref{thm:main-capacity}(b) that $\Well_T$ is empty for $T\ge1$ and that $\Well_T\subset(0,2)$. This proof is conditional on the results used from \cite{BM,CM,ABCHIM}, two classical Gaussian facts, and $802$ load inequalities behind Corollary~\ref{cor:load-bound}, computed outside Lean in ball arithmetic.

\section*{Acknowledgements}
We are grateful to Jean-Christophe Mourrat for his generous advice on writing this paper, and for sharing a draft of the introduction, whose order and some of whose phrasing we have followed.