Mathematical Physics

Motivation

Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for $E_8$ and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.

Timeline

• 1953–1964. Rankin, Cassels, Ennola and Diananda show that the triangular lattice minimizes the Epstein zeta function among planar lattices (doi:10.1017/S2040618500035668, doi:10.1017/S2040618500033906).
• 1988. Montgomery proves the Gaussian (theta-function) minimum among planar lattices of fixed covolume for every parameter (doi:10.1017/S0017089500007047).
• 2003. Cohn and Elkies introduce Fourier linear-programming bounds for sphere packing (doi:10.4007/annals.2003.157.689).
• 2007. Cohn and Kumar formulate the Euclidean universal-optimality program (Conjecture 9.4).
• 2018. Cohn and de Courcy-Ireland extend the Fourier comparison to density-based competitor classes (doi:10.1215/00127094-2018-0018).
• 2019. Radchenko and Viazovska develop Fourier interpolation on the line (doi:10.1007/s10240-018-0101-z).
• 2022. Cohn, Kumar, Miller, Radchenko and Viazovska prove universal optimality of $E_8$ and the Leech lattice (doi:10.4007/annals.2022.196.3.3).
• 2024–2025. Partial planar results: comparisons with periodic classes (Faulhuber–Shafkulovska–Zlotnikov, doi:10.1090/bproc/247), small periodic configurations (Hardin–Tenpas, doi:10.19086/da.144978), and local optimality under small displacements (Leblé, arXiv:2511.03353).

The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.

Setting

Let $b=\sqrt3/2$ and $A=b^{-1/2}\{m(1,0)+n(1/2,b):m,n\in\mathbb Z\}$, the triangular lattice of covolume one. Let $B_R$ be the closed disk of radius $R$ about the origin. A set $\mathcal C\subset\mathbb R^2$ is locally finite if each $\mathcal C\cap B_R$ is finite, and has centered disk density one if $N_R/(\pi R^2)\to1$, where $N_R=\#(\mathcal C\cap B_R)$.

A smooth $g:(0,\infty)\to[0,\infty)$ is completely monotone if $(-1)^jg^{(j)}(t)\ge0$ for all $j\ge0$, $t>0$. The lower energy per particle is

$$E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{N_R}\sum_{\substack{x,y\in\mathcal C\cap B_R\\ x\ne y}}g(|x-y|^2)\in[0,\infty],$$

summing over ordered pairs. The Fourier transform is $\widehat f(\xi)=\int f(x)e^{-2\pi i x\cdot\xi}\,dx$ and $A^*=\{\xi:\xi\cdot a\in\mathbb Z\ \forall a\in A\}$ is the dual lattice.

Formalization targets

Milestone: Theorem 1.2 (sharp Gaussian minorants)

For every $\alpha>0$ there is a real radial Schwartz $f_\alpha$ with

$$f_\alpha\le e^{-\pi\alpha|x|^2},\quad \widehat f_\alpha\ge0,\quad f_\alpha(a)=e^{-\pi\alpha|a|^2}\ (a\in A\setminus\{0\}),\quad \widehat f_\alpha(w)=0\ (w\in A^*\setminus\{0\}),$$

given for $\alpha\ge1$ by the paper's explicit atomic interpolation construction.

Goal: Theorem 1.1 (universal energy minimum)

For every smooth nonnegative completely monotone $g$ and every locally finite $\mathcal C$ of centered disk density one,

$$E_g(\mathcal C)\ \ge\ \sum_{a\in A\setminus\{0\}}g(|a|^2)\ =\ E_g(A)\qquad\text{in }[0,\infty].$$

Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.

Significance

Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as $t^{-p}$ with $p\le1$) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).

Difficulty

Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all $\alpha>0$ at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.

Formalization scope

• Points live in EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.
• AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), $g\ge0$ and $(-1)^r$ iteratedDeriv r g t $\ge0$ for $t>0$.
• energy g C is the liminf over $R\to\infty$ of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.
• The goal returns both the inequality for every admissible C and the equality latticeEnergy g = energy g A.
• For Theorem 1.2, realFourier is Mathlib's 𝓕 (kernel $e^{-2\pi i\langle x,\xi\rangle}$) applied to the complexified function; the $\alpha\ge1$ clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.

Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.

Selected references

• OpenAI, An atomic certificate for triangular-lattice universal optimality, preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf
• H. Cohn, A. Kumar, Universally optimal distribution of points on spheres, J. Amer. Math. Soc., 2007. https://doi.org/10.1090/S0894-0347-06-00546-7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, Universal optimality of the E8 and Leech lattices and interpolation formulas, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.3.3
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math., 2003. https://doi.org/10.4007/annals.2003.157.689
• H. Cohn, M. de Courcy-Ireland, The Gaussian core model in high dimensions, Duke Math. J., 2018. https://doi.org/10.1215/00127094-2018-0018
• H. L. Montgomery, Minimal theta functions, Glasgow Math. J., 1988. https://doi.org/10.1017/S0017089500007047
• R. A. Rankin, A minimum problem for the Epstein zeta-function, 1953. https://doi.org/10.1017/S2040618500035668
• D. Radchenko, M. Viazovska, Fourier interpolation on the real line, Publ. Math. IHÉS, 2019. https://doi.org/10.1007/s10240-018-0101-z
• T. Leblé, The hexagonal lattice is universally locally optimal, preprint, 2025. https://arxiv.org/abs/2511.03353

Motivation

Belief propagation (BP) is the message-passing algorithm used throughout artificial intelligence, coding theory and statistical physics to approximate marginals of graphical models. On graphs with cycles it is a heuristic: it may fail to converge, and when it converges its output need not be the true marginal. Rigorous guarantees had mostly been confined to the high-temperature regime, as a consequence of a uniform decay of correlations (spatial mixing) under which any boundary condition is forgotten; see the works cited as [3, 23, 26] in §1 of the paper.

Dembo and Montanari (arXiv:0804.4726v3, Ann. Appl. Probab. 20 (2010)) proved that for the ferromagnetic Ising model with a positive external field, BP converges exponentially fast on every graph of bounded degree, at every temperature, and that on locally tree-like graphs its fixed point computes local marginals accurately. The low-temperature regime, where the Gibbs measure on the limiting infinite tree is not unique, is the point: the field breaks the $\pm$ symmetry, and monotonicity replaces spatial mixing.

Setting

Let $G=(V,E)$ be a finite graph in which every vertex has at most $\Delta$ neighbours, $\beta\ge0$ an inverse temperature and $B$ a magnetic field. The Ising model on $G$ is the distribution on spin configurations $\underline x\in\{+1,-1\}^V$

$$\mu(\underline x)=\frac1{Z(\beta,B)}\exp\Big\{\beta\sum_{(i,j)\in E}x_ix_j+B\sum_{i\in V}x_i\Big\}.$$

More generally one allows a field $B_i$ at each vertex, and $B_i=+\infty$ (a vertex pinned to $+1$).

A message $\nu_{i\to j}$ is a distribution on $x_i\in\{+1,-1\}$ attached to the directed edge $i\to j$. The BP iteration is

$$\nu^{(t+1)}_{i\to j}(x_i)=\frac1{z^{(t)}_{i\to j}}\,e^{Bx_i}\prod_{l\in\partial i\setminus j}\ \sum_{x_l}e^{\beta x_ix_l}\,\nu^{(t)}_{l\to i}(x_l),$$

with $\partial i$ the neighbours of $i$ and $z^{(t)}_{i\to j}$ a normalization. An initial condition is positive if $\nu^{(0)}_{i\to j}(+1)\ge\nu^{(0)}_{i\to j}(-1)$ on every directed edge. Distances between distributions are in total variation, $\|p-q\|_{\mathrm{TV}}=\tfrac12\sum_x|p(x)-q(x)|$.

For $i_*\in V$, $U=\mathsf B_{i_*}(r)$ is the ball of radius $r$, $\partial U$ its vertices at distance exactly $r$, and $j(i)$ a neighbour in $U$ of each $i\in\partial U$. Given a BP fixed point $\nu^*$, the BP estimate of the marginal on $U$ is

$$\nu_U(\underline x_U)=\frac1{z_U}\exp\Big\{\beta\sum_{(i,j)\in E_U}x_ix_j+B\sum_{i\in U\setminus\partial U}x_i\Big\}\prod_{i\in\partial U}\nu^*_{i\to j(i)}(x_i).$$

The proofs run through Ising models on rooted trees $\mathsf T$: $\mathsf T(\ell)$ is the tree of the first $\ell$ generations, $\partial\mathsf T(\ell)$ the $\ell$-th generation, and $\mu^{\ell,0}$, $\mu^{\ell,+}$ the Ising models on $\mathsf T(\ell)$ with free and plus boundary conditions (the latter pins $\partial\mathsf T(\ell)$ to $+1$). A random tree is conditionally independent with average offspring bounded by $\Delta$ if, given the first $k$ generations, the offspring numbers of generation $k$ are independent with conditional means at most $\Delta$ (Definition 2.5).

Formalization targets

Goal: Theorem 2.6

For $\beta\ge0$, $B>0$ and $\Delta$, there are $A<\infty$ and $\lambda>0$ depending only on $(\beta,B,\Delta)$ such that every finite graph of maximal degree $\Delta$ has a BP fixed point $\nu^*$ with

$$\sup_{(i,j)\in E}\big\|\nu^{(t)}_{i\to j}-\nu^*_{i\to j}\big\|_{\mathrm{TV}}\le A\exp(-\lambda t)$$

for every positive initial condition and every $t\ge0$. The constants are uniform over graphs; this uniformity is the content of the theorem.

Companion: Theorem 2.7

With $c=c(\beta,B,\Delta)$ and $\lambda>0$: if $\mathsf B_{i_*}(t)$ is a tree, then $\|\mu_U-\nu_U\|_{\mathrm{TV}}\le\exp\{c^{r+1}-\lambda(t-r)\}$.

Milestones

The tree estimates of §3–§4, in the order the proofs use them: Griffiths' inequality (Theorem 3.1); the GHS inequality (Theorem 3.2); the reweighting bound in total variation (Lemma 3.3); marginals on subtrees (Lemma 4.1); the $M/\ell$ bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le M/\ell$ on root magnetizations (Lemma 4.3); its extension to marginals near the root (Theorem 4.2); a Simon-type factorization of tree correlations (Lemma 4.4); and Corollary 4.5: exponential decay of correlations (4.13), Theorem 4.2 with rate $Ae^{-\lambda t}$, and the root-magnetization bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le Ae^{-\lambda\ell}$.

Significance

The theorem gives an unconditional convergence guarantee for BP on a nontrivial class of models with cycles, valid deep in the low-temperature phase, with a rate independent of the number of vertices. Theorem 2.7 adds that the fixed point is accurate on locally tree-like graphs such as random regular graphs and sparse Erdős–Rényi graphs, so BP is a polynomial-time algorithm for local marginals there. The tree estimates of §4, in particular the insensitivity of the root to plus versus free boundary conditions on conditionally independent trees, are also the engine of the free-entropy theorem of the same paper (mission 1 of this series).

The results are proved in the paper; none of them, nor Griffiths' or the GHS inequality, has a machine-checked proof known to this mission. Formalizing them produces a reusable library for ferromagnetic Ising models on finite graphs and trees (correlation inequalities, pinned boundary conditions, marginals on subtrees) and a formal account of BP as an operator on message families.

Difficulty

The obvious argument is a contraction: show that one BP step shrinks the distance between message families, uniformly over the graph. At low temperature this fails: the BP map is not a contraction, the infinite-tree Ising model has several Gibbs measures, and without a field BP has several fixed points. Uniform decay of correlations, the tool behind high-temperature results, is false in this regime. What has to be controlled instead is a single, weaker quantity: how much the root of a tree of depth $t$ feels a plus boundary condition compared with a free one, with a bound that is uniform over all trees of bounded average offspring and over all depths. The difficulty is concentrated in that estimate (Lemma 4.3), and in upgrading its $1/\ell$ rate to an exponential one (Corollary 4.5), which is where the positive field enters quantitatively.

Formalization scope

Spins are Booleans (true $=+1$); the edge sum counts each unordered edge once; a field $+\infty$ is a pinned vertex, never a large real number. Graphs are finite (Fintype V) with all degrees at most $\Delta$. Messages are functions on ordered vertex pairs whose values on directed edges are distributions on $\{+1,-1\}$; the BP iterates are computed from the update, not posited. Total variation is $\tfrac12\ell^1$. Trees are encoded by offspring functions on finite words (Ulam–Harris), random trees by probability measures on offspring functions with the product $\sigma$-algebra; conditional independence uses Mathlib's iCondIndepFun, with integrable offspring numbers. Fields on trees are nonrandom functions of the vertex. Expectations that may be infinite, such as $\mathbb E\{C^{|\mathsf T(r)|}\}$, are lower Lebesgue integrals in $[0,\infty]$, and every expectation of a tree functional comes with a measurability conclusion, so that no integral can take a junk value. Constants are quantified before the graph, the tree law and the field, and, where the paper names their dependence (Theorem 4.2's $M(\beta_{\max},B_{\min},\Delta)$ and $C(\beta_{\max},B_{\max})$), as functions of exactly those parameters.

Two readings are fixed explicitly. Theorem 2.7 is stated for every positive BP fixed point, which by Theorem 2.6 is the paper's fixed point. Corollary 4.5's clause (4.13) carries the hypotheses of Theorem 4.2 ($B_i\le B_{\max}$ on $\mathsf T(r-1)$). A fixed point that is not a family of distributions, a "zero message" family, or a bound that holds only because an integral defaults to $0$ does not satisfy these statements.

The computation tree of §5, through which the paper derives Theorems 2.6–2.7 from Corollary 4.5, is a proof device and is not part of any statement; building it is welcome as supporting work. Proofs of the classical inequalities (Griffiths, GHS) are independently reusable.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. arXiv:0804.4726v3, doi:10.1214/09-AAP627
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. MR0266507
• T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). MR776231
• B. Simon, Correlation inequalities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980) 111–126. MR589426

Motivation

The ferromagnetic Ising model is the basic model of statistical mechanics for interacting binary variables. On a finite graph it is a probability distribution over spin configurations, and its normalizing constant, the partition function, encodes the thermodynamics: the free entropy per vertex determines the magnetization, the correlations, and the location of phase transitions. On lattices this quantity is understood only in special cases. On sparse random graphs, such as random regular graphs and Erdős–Rényi graphs with bounded average degree, physicists predicted it with the cavity method (Mézard and Parisi, The Bethe lattice spin glass revisited, 2001): locally these graphs look like trees, and on trees the model can be solved by a recursion. The same recursion underlies belief propagation, the message-passing algorithm used in coding theory and machine learning.

Timeline:

• Dembo and Montanari (2008/2010), Ising models on locally tree-like graphs, Ann. Appl. Probab. 20 (2010) 565–592: for every uniformly sparse graph sequence converging locally to a Galton–Watson tree whose offspring law has finite mean, the free entropy density converges at every temperature $\beta \ge 0$ and every field $B$, and for $B > 0$ the limit is the Bethe prediction. Earlier rigorous results covered special cases, among them Erdős–Rényi graphs in a restricted range of parameters (reference [7] of the paper) and random regular graphs (reference [11]).
• Dembo, Montanari and Sun (2013), Factor models on locally tree-like graphs, extended the approach to a class of factor models on locally tree-like graphs.

Setting

Let $G_n = (V_n = [n], E_n)$ be a sequence of finite graphs. The Ising measure at inverse temperature $\beta \ge 0$ and magnetic field $B \in \mathbb R$ is

$$\mu(\underline x) = \frac{1}{Z_n(\beta,B)} \exp\Big\{\beta \sum_{(i,j)\in E_n} x_i x_j + B \sum_{i \in V_n} x_i\Big\}, \qquad x_i \in \{+1,-1\},$$

each edge counted once, and the free entropy density is $\phi_n(\beta,B) = \frac1n \log Z_n(\beta,B)$.

A degree distribution is a law $P = \{P_k\}$ on $\{0,1,2,\dots\}$ with $0 < \bar P = \sum_k k P_k < \infty$; its size-biased version is $\rho_k = k P_k/\bar P$, and $\bar\rho = \sum_k (k-1)\rho_k$. The Galton–Watson tree $T(P,\rho,\infty)$ has a root with $k$ children with probability $P_k$, and every other vertex independently has $k-1$ children with probability $\rho_k$; $T(P,\rho,t)$ is its first $t$ generations.

The ball $B_i(t)$ is the subgraph induced by the vertices within distance $t$ of $i$, rooted at $i$. The sequence converges locally to $T(P,\rho,\infty)$ if, for every $t$ and every rooted tree $T$, the fraction of vertices $i$ with $B_i(t) \simeq T$ (root-preserving isomorphism) tends to $\mathbb P\{T(P,\rho,t) \simeq T\}$. It is uniformly sparse if $\lim_{l\to\infty}\limsup_n \frac1n\sum_i |\partial i|\,\mathbb I(|\partial i| \ge l) = 0$.

The cavity recursion acts on laws of a real random variable $h$:

$$h \overset{d}{=} B + \sum_{i=1}^{K-1} \xi(\beta, h_i), \qquad \xi(\beta,h) = \operatorname{atanh}[\tanh\beta \tanh h],$$

with $K \sim \rho$ and $h_i$ i.i.d. copies of $h$ independent of $K$. For $B > 0$ it has a unique fixed point $h^*$ supported on $[0,\infty)$. The Bethe functional of a law of $h$ is

$$\varphi_h(\beta,B) = \frac{\bar P}{2}\log\cosh\beta - \frac{\bar P}{2}\mathbb E\log[1+\tanh\beta\tanh h_1\tanh h_2] + \mathbb E\log\Big\{e^B\prod_{i=1}^L[1+\tanh\beta\tanh h_i] + e^{-B}\prod_{i=1}^L[1-\tanh\beta\tanh h_i]\Big\},$$

with $L \sim P$ independent of the $h_i$.

Formalization targets

Goal: Theorem 2.4

Assume $\{G_n\}$ is uniformly sparse, converges locally to $T(P,\rho,\infty)$, and $\sum_k k\rho_k < \infty$. Then for every $\beta \ge 0$:

$$\lim_{n\to\infty}\phi_n(\beta,B) = \varphi_{h^*}(\beta,|B|) \quad (B \ne 0),$$

and $\varphi_{h^*}(\beta,B)$ has a limit $L_0$ as $B \downarrow 0$, with $\phi_n(\beta,0) \to L_0$. This is the paper's statement that the limit exists for every $B$, equals (2.9) for $B > 0$, is even in $B$, and is continuous at $B = 0$.

Milestones

1. Tools on Ising models: Griffiths' inequality (Theorem 3.1), the GHS inequality (Theorem 3.2), the subtree-marginal identity (Lemma 4.1).
2. Trees: the boundary effect on the root magnetization, $\mathbb E\{m^{\ell,+}-m^{\ell,0}\} \le M/\ell$ (Lemma 4.3); the correlation factorization (Lemma 4.4); exponential decay of root-to-generation correlations (Corollary 4.5, (4.13)).
3. The recursion: monotone convergence to the unique nonnegative fixed point (Lemma 2.3) and its Lipschitz dependence on $\beta$ in Monge–Kantorovich distance (Lemma 4.6).
4. The Bethe functional: the second-order perturbation bound (Lemma 6.1, Remark 6.2) and its consequence, stationarity of $\varphi_h$ at fixed points (Corollary 6.3, with corrected constant).
5. From trees to graphs: edge averages converge to averages over the edge-rooted tree $\bar T(\rho,t)$ (Lemma 6.4), and $\partial_\beta\phi_n = \frac1n\sum_{(i,j)\in E_n}\langle x_ix_j\rangle_n$ (6.10).

Significance

The result. Theorem 2.4 establishes the replica-symmetric (Bethe) formula for the ferromagnetic Ising model on the standard sparse random graph ensembles at all temperatures, including below the critical temperature $\tanh\beta_c = 1/\bar\rho$ where the Gibbs measure on the limiting tree is not unique. It identifies the free energy of random regular graphs, Erdős–Rényi graphs and configuration models with arbitrary degree distributions of finite variance, and the derivative identities that follow give the limiting magnetization and energy per edge. The tree estimates of Section 4 also yield the convergence of belief propagation (the companion mission of this series).

Formalizing it. The theorem is proved; nothing in this mission has been machine-checked before. A formal proof requires infrastructure that Lean's Mathlib does not have: Ising measures with boundary conditions, correlation inequalities, Galton–Watson trees as laws of offspring functions, local weak convergence of graph sequences, distributional fixed-point equations, and the Monge–Kantorovich distance on the real line. While stating the milestones, Corollary 6.3 turned out to be false as printed (the constant $\bar P\bar\rho$ should be $\mathbb E[L^2]$; a counterexample is $P = \delta_1$); the mission states the corrected version, which is what the paper's proof gives.

Difficulty

The obvious route through uniqueness of the Gibbs measure on the tree fails below the critical temperature: different boundary conditions give different limits, so local quantities are not determined by the local graph structure alone. The paper replaces uniqueness by insensitivity to positive boundary conditions when $B > 0$ (Lemma 4.3), which rests on Griffiths and GHS monotonicity and on averaging over the random tree; the deterministic statement is false. Passing from derivatives to the free entropy itself requires that the Bethe functional be stationary in the cavity law (Corollary 6.3), so that the $\beta$-dependence of $h^*$ can be ignored. Finally, the case $B = 0$ at low temperature is reached only as a limit: there is no fixed-point characterization at $B = 0$.

Formalization scope

• Spins are Booleans ($+1$ = true); edges are unordered and counted once. Graphs $G_n$ live on Fin n.
• A field $B_i = +\infty$ (plus boundary) is encoded by pinning vertex $i$ to $+1$, never by a large real field.
• Rooted trees are offspring functions List ℕ → ℕ in Ulam–Harris form; random trees are laws of offspring functions under the product σ-algebra. Galton–Watson trees are infinite product measures. Fields on trees are nonrandom functions of the vertex.
• Laws of cavity fields are probability measures on $\mathbb R$; the recursion is a map on ProbabilityMeasure ℝ, and convergence in distribution is weak convergence. Expectations over $L \sim P$ are series $\sum_l P_l\,\mathbb E[\cdot]$ with product laws.
• The Monge–Kantorovich distance takes values in $[0,\infty]$. Uniform sparsity is computed in $[0,\infty]$ so that an unbounded sequence does not get a junk $\limsup$ of $0$.
• The fixed point $h^*$ in the goal is the one supported on $[0,\infty)$, selected by choice; Lemma 2.3 shows it exists and is unique, so an arbitrary fixed point cannot be substituted. Theorem 2.4 is stated with $\beta \ge 0$ and asserts convergence for $B > 0$, $B < 0$ and $B = 0$ separately; the $B = 0$ clause asserts the existence of the one-sided limit rather than assuming it.

A complete development needs: Griffiths and GHS inequalities for finite Ising models (reusable for any ferromagnetic model); Ulam–Harris random trees with conditional independence; local weak convergence of graph sequences (reusable for random graph theory); distributional recursions with stochastic ordering; and the coupling characterization of the Wasserstein-1 distance on $\mathbb R$. Contributions of any milestone are welcome, as are proofs of the classical inequalities of Section 3 independent of this paper.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. https://arxiv.org/abs/0804.4726v3 , https://doi.org/10.1214/09-AAP627
• M. Mézard, G. Parisi, The Bethe lattice spin glass revisited, Eur. Phys. J. B 20 (2001) 217–233. https://doi.org/10.1007/PL00011099
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. https://doi.org/10.1063/1.1665211
• T. M. Liggett, Interacting Particle Systems, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). https://doi.org/10.1007/978-1-4613-8542-4
• A. Dembo, A. Montanari, N. Sun, Factor models on locally tree-like graphs, Ann. Probab. 41(6) (2013) 4162–4213. https://doi.org/10.1214/12-AOP828

Motivation

The ground-state energy of a mixed $p$-spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$, converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$. Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$. This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$, with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$. Its derivatives $\xi'$, $\xi''$ are nonnegative and nondecreasing on $[0,1]$.

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

$$\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .$$

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$.

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

$$\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .$$

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$, for $t\in[t_{i-1},t_i)$,

$$\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.$$

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$.

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$, progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$, with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$. The value is

$$\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}$$

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$,

$$V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .$$

Formalization targets

Goal: Proposition 4.1

$$\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .$$

Milestones

1. Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$, with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$, it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$.
2. Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$, where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$.
3. Lemma 7.3: $V$ solves the HJB equation

$$\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .$$

4. Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$.
5. Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$.

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$, which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ($M_1\in(-1,1)$), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$.

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$, where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$. The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

• Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
• Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$; its value at $t=1$ never matters.
• Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$, the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
• Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
• Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$, where it is bounded below.
• Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$, with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$.
• Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$.
• Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as "$v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
• Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$, and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
• Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$, which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
• N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

Motivation

The mixed $p$-spin model is a random polynomial on the hypercube $\{-1,+1\}^N$: a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$. Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$. The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$-spin models with $p \ge 3$. This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$-spin models and introduced the extended principle over $\mathscr L$.

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$, with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$, in one of two spaces:

$$\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.$$

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$, and $\mathscr U \subseteq \mathscr L$.

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$), the Parisi PDE

$$\partial_t\Phi + \tfrac12\xi''(t)\big(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\big) = 0,\qquad \Phi(1,x) = |x|,$$

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$. For general $\gamma \in \mathscr L$, $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$. The Parisi functional is

$$\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .$$

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$, $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$.

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$, then

$$\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .$$

Since $\mathscr U \subseteq \mathscr L$, this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

1. Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$, $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$.
2. Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$, for admissible directions $\delta$ that vanish near $t = 1$.
3. Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$.
4. Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$.

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$-approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$. It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$, which is generally non-zero near $t = 1$, where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

• Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$. $\xi'$ and $\xi''$ are explicit power series.
• Order parameters. Functions $\mathbb R\to\mathbb R$; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$. Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
• Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$. The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$. Gaussian expectations are integrals against gaussianReal 0 1.
• $\Phi^\gamma$ on $\mathscr L$. limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$.
• SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$. Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
• Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
• Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$. For $\xi\equiv0$ it is false: $\mathsf P\equiv0$, $X\equiv0$, and the left side is constant in $t$. The goal does not need it.
• Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
• Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
• Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144(7), 2016. https://arxiv.org/abs/1502.04398
• A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
• M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

Motivation

In a scattering experiment a particle arrives from far away, interacts with a target, and leaves again. Far from the target the forces are negligible, so long before and long after the collision the particle should move like a free particle. Scattering theory makes this precise by comparing two quantum dynamics: the free evolution $\mathrm e^{-\mathrm itH_0}$ generated by the kinetic energy $H_0 = -\Delta$, and the full evolution $\mathrm e^{-\mathrm itH}$ generated by $H = H_0 + V$. The objects that compare them are the wave operators (Møller operators) $\Omega_\pm$, introduced by Møller (1945) and put on a rigorous footing by Jauch (1958) and Kato. Cook (1957) gave the first practical criterion for their existence. Kuroda, Birman, Agmon, Enß and others later developed the theory up to asymptotic completeness for short-range potentials.

This mission formalizes the abstract part of Chapter 12 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the definition and basic structure of the wave operators, Cook's criterion, and the existence of the wave operators for a square-integrable potential in three dimensions.

Setting

Let $\mathfrak H$ be a complex Hilbert space. An operator $A$ is a linear map on a subspace $\mathfrak D(A)$, its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A = A^*$. A projection-valued measure $P$ assigns to each Borel set $\Omega \subseteq \mathbb R$ an orthogonal projection $P(\Omega)$, with $P(\mathbb R) = \mathbb I$ and $P(\bigcup_n\Omega_n)\psi = \sum_n P(\Omega_n)\psi$ for disjoint $\Omega_n$. The spectral measure of $\psi$ is $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle$. By the spectral theorem every self-adjoint $A$ equals $\int\lambda\,dP(\lambda)$ for a unique $P$: $\mathfrak D(A) = \{\psi \mid \int\lambda^2\,d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\,d\mu_\psi$. The time evolution $\mathrm e^{-\mathrm itA}$ is the bounded operator with $\langle\psi, \mathrm e^{-\mathrm itA}\psi\rangle = \int\mathrm e^{-\mathrm it\lambda}\,d\mu_\psi(\lambda)$.

For two self-adjoint operators $H_0$, $H$ the wave operators are

$$\mathfrak D(\Omega_\pm) = \{\psi \in \mathfrak H \mid \exists\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi\}, \qquad \Omega_\pm\psi = \lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi .$$

$\mathfrak D(\Omega_\pm)$ is the set of asymptotic states and $\operatorname{Ran}(\Omega_\pm) = \Omega_\pm\mathfrak D(\Omega_\pm)$ the set of states that have one. A closed subspace $\mathfrak H_1$ with projection $P_1$ reduces $A$ if $P_1\mathfrak D(A) \subseteq \mathfrak D(A)$ and $P_1A\psi = AP_1\psi$ for $\psi \in \mathfrak D(A)$.

On $L^2(\mathbb R^n)$ the free Schrödinger operator is $H_0 = -\Delta$ with domain the Sobolev space $H^2(\mathbb R^n)$: under the Fourier transform it is multiplication by $p^2$ on $\{\varphi \mid p^2\varphi \in L^2\}$. For a real potential $V$, $H = H_0 + V$ has $\mathfrak D(H) = H^2(\mathbb R^n)$ and $(H\psi)(x) = (H_0\psi)(x) + V(x)\psi(x)$.

Formalization targets

Goal: existence of the wave operators for $V \in L^2(\mathbb R^3)$ (Theorem 12.4)

Let $H_0$ be the free Schrödinger operator on $L^2(\mathbb R^3)$ and $H = H_0 + V$ with a real $V \in L^2(\mathbb R^3)$. Then

$$\mathfrak D(\Omega_+) = \mathfrak D(\Omega_-) = L^2(\mathbb R^3),$$

that is, $\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ exists for every $\psi$ and both signs. Since the spectrum of $H_0$ is purely absolutely continuous, this is exactly what Teschl calls "the wave operators exist" (12.14).

Milestones

• Lemma 12.1. $\mathfrak D(\Omega_\pm)$ and $\operatorname{Ran}(\Omega_\pm)$ are closed and $\Omega_\pm : \mathfrak D(\Omega_\pm) \to \operatorname{Ran}(\Omega_\pm)$ is unitary.
• Theorem 12.2. $\mathfrak D(\Omega_\pm)$ reduces $H_0$, $\operatorname{Ran}(\Omega_\pm)$ reduces $H$, and the restricted operators are unitarily equivalent: $\Omega_\pm H_0\psi = H\Omega_\pm\psi$ for $\psi \in \mathfrak D(\Omega_\pm) \cap \mathfrak D(H_0)$.
• Lemma 12.3 (Cook). If $\mathfrak D(H) \subseteq \mathfrak D(H_0)$, $\psi \in \mathfrak D(H_0)$ and $\int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt < \infty$, then $\psi \in \mathfrak D(\Omega_\pm)$ and $\|(\Omega_\pm - \mathbb I)\psi\| \le \int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt$.

Significance

Existence of the wave operators is the first step of every scattering theory for Schrödinger operators: without it the scattering operator $S = \Omega_+^{-1}\Omega_-$ is not defined on a useful set of states, and the questions of completeness and asymptotic completeness (Enß's theorem, Theorem 12.12 of the same chapter) cannot be posed. Lemma 12.1 and Theorem 12.2 are the structural facts that make $\Omega_\pm$ partial isometries intertwining the two Hamiltonians; they imply that $H$ restricted to $\operatorname{Ran}(\Omega_\pm)$ has absolutely continuous spectrum whenever $H_0$ does, and that kinetic energy is conserved in scattering. Cook's criterion is the tool used in practice to prove existence for concrete potentials, including Coulomb-type and time-dependent problems.

The results are classical and proved in the literature. They are not formalized. Mathlib has neither the spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no scattering theory. The platform has no statement about wave operators; its BookProof development contains Stone's theorem for its own structure of unbounded operators, which this mission does not use.

Difficulty

The limit defining $\Omega_\pm$ involves two unitary groups whose generators do not commute, and neither group is explicit for the perturbed operator $H$. For Cook's criterion the product $\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ has to be differentiated in $t$, which needs control of domains: $\mathrm e^{-\mathrm itH_0}\psi$ must stay in the domain of $H - H_0$, and the derivative of a strongly continuous unitary group exists only on the domain of its generator. For the goal, the time evolution of a general $\psi \in L^2(\mathbb R^3)$ has no decay rate at all, and the potential $V \in L^2$ is unbounded and has no decay assumption beyond square integrability, so the integrability condition of Cook's criterion cannot be checked for every $\psi$ directly. The intertwining relation (12.8) concerns unbounded operators and needs the reduction of the domains, not only an identity between bounded operators.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint. Separability is not assumed.

The spectral theorem is not part of this mission. Every statement takes projection-valued measures $P_0$ and $P$ as data, with the hypotheses $H_0 = \int\lambda\,dP_0(\lambda)$ and $H = \int\lambda\,dP(\lambda)$ (domain and quadratic form as above), which is the form the spectral theorem guarantees and which determines $P_0$ and $P$. The time evolutions are $\mathrm e^{-\mathrm itH_0} = \int\mathrm e^{-\mathrm it\lambda}\,dP_0$ and $\mathrm e^{-\mathrm itH} = \int\mathrm e^{-\mathrm it\lambda}\,dP$. In the goal, the self-adjointness of $H = H_0 + V$ (Theorem 10.2 of the book) enters only through the existence of $P$. Nothing is assumed about $\Omega_\pm$.

The sign of $\Omega_\pm$ is a unit s : ℤˣ, and $t \to \pm\infty$ is written as $t \to +\infty$ in the variable $st$. $\Omega_\pm$ is Mathlib's limUnder and is used only on $\mathfrak D(\Omega_\pm)$. A formalization that set $\Omega_\pm\psi = 0$ where the limit fails and then proved only that $\Omega_\pm$ is isometric would lose the content of the goal; here the goal asserts that the limit exists for every $\psi \in L^2(\mathbb R^3)$. In Cook's lemma the finiteness of the integral is integrability on $(0,\infty)$, the bound uses the Bochner integral, and the hypothesis that $\exp(\mp\mathrm itH_0)\psi$ lies in $\mathfrak D(H)$ for $t \ge 0$, which the integrand presupposes, is explicit.

$L^2(\mathbb R^3)$ is Mathlib's Lp ℂ 2 on EuclideanSpace ℝ (Fin 3). The free Schrödinger operator is characterized through Mathlib's unitary $L^2$ Fourier transform $\mathcal F_M f(\xi) = \int\mathrm e^{-2\pi\mathrm i\langle x,\xi\rangle}f(x)\,dx$, not the book's $(2\pi)^{-n/2}\int\mathrm e^{-\mathrm ipx}f(x)\,dx$. The constants are translated: $\mathfrak D(H_0) = \{\psi \mid |\xi|^2\mathcal F_M\psi \in L^2\}$ and $\mathcal F_M(H_0\psi) = 4\pi^2|\xi|^2\mathcal F_M\psi$. $H = H_0 + V$ has $\mathfrak D(H) = \mathfrak D(H_0)$ and $H\psi = H_0\psi + V\psi$ almost everywhere.

A complete development needs a functional calculus for projection-valued measures (strong continuity and differentiability of $\mathrm e^{-\mathrm itA}$ on $\mathfrak D(A)$, Theorem 5.1), the explicit $L^1 \to L^\infty$ decay of the free Schrödinger group in $\mathbb R^3$ ((7.31) of the book), and density of $L^1 \cap H^2$ in $L^2$. These pieces are reusable for the rest of Chapter 12 (incoming and outgoing states, short-range potentials, asymptotic completeness). Proofs of any milestone and of such supporting lemmas are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Chapter 12, pp. 247–257.
• J. M. Cook, Convergence to the Møller wave-matrix, J. Math. and Phys. 36 (1957), 82–87. doi:10.1002/sapm195736182.
• J. M. Jauch, Theory of the scattering operator, Helv. Phys. Acta 31 (1958), 127–158.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics III: Scattering Theory, Academic Press, 1979.
• V. Enß, Asymptotic completeness for quantum mechanical potential scattering. I. Short range potentials, Comm. Math. Phys. 61 (1978), 285–291. doi:10.1007/BF01940771.