Mathematical Physics

Motivation

Simulating the time evolution $e^{-iHt}$ of a many-body Hamiltonian is one of the main proposed uses of quantum computers. For a Hamiltonian $H = \sum_X h_X$ whose terms act on small, nearby groups of sites of a lattice, Haah, Hastings, Kothari and Low give a quantum algorithm whose gate count is nearly linear in the space-time volume $n t$, and show that this is optimal up to logarithmic factors. The algorithm decomposes $e^{-iHt}$ into evolutions of overlapping blocks, and the error of each step is controlled by a Lieb–Robinson bound: in a locally interacting system, an operator evolved for time $t$ stays, up to a superexponentially small error, inside a region whose size grows linearly with $t$.

Lieb–Robinson bounds go back to Lieb and Robinson (1972), who proved a finite propagation speed for quantum spin systems. Hastings (2004), Nachtergaele and Sims (2006) and Hastings and Koma (2006) gave the commutator form used today and applied it to the decay of correlations in gapped ground states. Appendix C of the paper re-derives the bound in a self-contained way. Section C.4 treats strictly local interactions, where every term is supported on a set of diameter at most $1$, and obtains a bound with an explicit factor $(2\zeta_0|t|)^\ell/\ell!$. This mission formalizes that bound.

Setting

Let $\Lambda$ be a finite set of sites with a metric $\mathrm{dist}$. Every site carries $\mathbb{C}^q$, and operators act on $\bigotimes_{x \in \Lambda} \mathbb{C}^q$; all norms $\|\cdot\|$ are operator norms. An operator is supported on $X \subseteq \Lambda$ if it has the form $m \otimes \mathbb{1}_{\Lambda \setminus X}$. For finite sets of sites, $\mathrm{dist}(X, Y) = \min_{x \in X, y \in Y} \mathrm{dist}(x, y)$, $\mathrm{diam}(X) = \max_{x, x' \in X} \mathrm{dist}(x, x')$, and $X \sim Y$ means $X \cap Y \ne \emptyset$.

A Hamiltonian is a family $(h_X)_{X \subseteq \Lambda}$ of Hermitian operators, $h_X$ supported on $X$, with $H = \sum_{X \subseteq \Lambda} h_X$; for a region $\Omega$, $H_\Omega = \sum_{Z \subseteq \Omega} h_Z$. The Heisenberg evolution of an operator $O$ is $O(t; J) = e^{iJt} O e^{-iJt}$, and $O(t) = O(t; H)$. The interaction is strictly local if $h_X = 0$ whenever $\mathrm{diam}(X) > 1$, and its strength is measured by

$$\zeta_0 = \max_{x \in \Lambda} \sum_{Q \ni x} |Q|\, \|h_Q\| .$$

The proof works with two auxiliary quantities attached to a fixed operator $B$ supported on $Y$:

$$C_B(X, t) = \sup_{A \in \mathcal{A}_X,\ \|A\| \le 1} \|[A(t), B]\|, \qquad D_B(X, t) = \|[h_X(t), B]\|,$$

where $\mathcal{A}_X$ is the algebra of operators supported on $X$. A tuple $(Z_1, \dots, Z_k)$ is linked from $X$ if $X \sim Z_1 \sim \cdots \sim Z_k$.

Formalization targets

Goal: display (48)

For $A$ supported on $X$, $B$ supported on $Y$, $\ell = \lfloor \mathrm{dist}(X, Y) \rfloor$ and every real $t$,

$$\|[A(t), B]\| \le 2\,\|A\|\,\|B\|\,|X|\,\frac{(2\zeta_0|t|)^{\ell}}{\ell!} .$$

Milestones

1. The elementary bounds (28): $C_B(Z, 0) \le 2\|B\|\delta_{Z \sim Y}$, $C_B(Z, t) \le 2\|B\|$, and the same for $D_B$ with an extra factor $\|h_Z\|$.
2. The integral inequality (24): $C_B(X, t) \le C_B(X, 0) + \sum_{Z \sim X} 2\int_0^{|t|} D_B(Z, s)\, ds$.
3. The closed recursion (42): $C_B(X, t) \le C_B(X, 0) + 2\sum_{Z : X \sim Z} \|h_Z\| \int_0^{|t|} C_B(Z, s)\, ds$.
4. The truncated iteration (44): $C_B(X, t) \le 2\|B\| \frac{(2|t|)^\ell}{\ell!} \sum_{Z_1, \dots, Z_\ell : \text{linked}} \prod_j \|h_{Z_j}\|$.
5. The counting bounds (45)–(46): $\sum_{Q : P \sim Q \sim S} \|h_Q\| \le \zeta_0 \sum_{p \in P} \delta_{\mathrm{dist}(p, S) \le 1}$ and its weighted, distance-tracking companion.
6. Lemma 5, eq. (4) = (49): $\|O_X(t; H) - O_X(t; H_\Omega)\| \le |X|\,\|O_X\|\,(2\zeta_0|t|)^\ell/\ell!$ with $\ell = \lfloor \mathrm{dist}(X, \Lambda \setminus \Omega) \rfloor$, under the added hypothesis $\mathrm{dist}(X, \Lambda \setminus \Omega) \ge 1$.

The goal is (48) rather than Lemma 5 because (48) is proved in full on pp. 26–27, while Lemma 5 is obtained "by manipulation analogous to Eq. (39)" and is false as printed when $\ell = 0$.

Significance

The bound (48) states that commutators with distant operators are suppressed by a factor that, at fixed $t$, decays faster than any exponential in the distance. The same factor controls Lemma 5, which is what the decomposition lemmas of the paper (Lemma 6 and its corollaries) use to bound the error of replacing a global evolution by evolutions of overlapping blocks; that in turn gives the paper's gate counts. Bounds of this type also underlie the exponential clustering of correlations in gapped ground states and the quasi-adiabatic continuation technique.

The results are proved in the literature and in this paper. A search of the local Prove2Me prior-art index found no matching formal statement for this finite spin-system bound. The mission seeks a machine-checked proof of the strictly local bound with its explicit constant, together with reusable infrastructure: operators supported on subsets of a tensor product of matrix algebras, their Heisenberg evolution, and an integral inequality for commutator growth.

Difficulty

The obvious argument expands $A(t) = \sum_k (it)^k \mathrm{ad}_H^k(A)/k!$ and notes that the first $\ell$ nested commutators with $B$ vanish. This does not give the stated bound: the norm of $\mathrm{ad}_H^k(A)$ grows like $k!$ times the number of growing clusters of terms, and the tail of the series is not controlled by its leading term. The explicit factor $(2\zeta_0|t|)^\ell/\ell!$, with no exponential prefactor, requires precise control of the time-dependent supremum $C_B(Z,s)$ and the combinatorics of linked chains. A second difficulty is Lemma 5, whose printed form is false at $\ell = 0$ and whose proof in the paper is a one-line reference to an analogous computation.

Formalization scope

Sites are an arbitrary finite metric space $\Lambda$ ([Fintype Λ] [MetricSpace Λ]); operators are matrices Matrix (Λ → Fin q) (Λ → Fin q) ℂ in the product basis, with the same local dimension $q$ at every site. This generalizes the paper's qubits on a lattice in $\mathbb{R}^D$. The norm is the $L^2$ operator norm (Matrix.Norms.L2Operator), never the entrywise or Frobenius norm. SupportedOn X M states $M = m \otimes \mathbb{1}$ entrywise, and is not vacuous: a nonzero operator on a single site satisfies it, and only scalars are supported on $\emptyset$. The Hamiltonian is time-independent and sums over every subset of $\Lambda$; strict locality is the hypothesis $1 < \mathrm{diam}(X) \Rightarrow h_X = 0$ on the terms. The constant $\zeta_0$ is carried as an upper bound of the site sums $\sum_{Q \ni x} |Q|\,\|h_Q\|$, which is equivalent to the paper's maximum for these monotone bounds; no bound $\|h_X\| \le 1$ is assumed. $\mathrm{dist}(X, Y)$ is a minimum over nonempty sets and $0$ if a set is empty, $\ell$ is its natural-number floor, and $C_B$ is a real supremum over a nonempty set bounded by $2\|B\|$. The integral milestones (24) and (42) are stated for $t \ge 0$; the goal, (44) and Lemma 5 hold for every real $t$. Lemma 5 carries one disclosed added hypothesis, $\mathrm{dist}(x, y) \ge 1$ for $x \in X$, $y \notin \Omega$, without which it is false.

None of the statements is trivialized: the goal mentions neither $C_B$ nor linked sums, its norm is the operator norm, the integrals are of continuous functions on compact intervals, the supremum is over a nonempty bounded set, and no disjointness of $X$ and $Y$ is assumed, so it covers $\ell = 0$ as well.

A complete development needs the derivative of $t \mapsto e^{iHt} A e^{-iHt}$, unitarity of $e^{iHt}$ for Hermitian $H$, commutation of operators with disjoint supports, Grönwall-type iteration of integral inequalities, and the simplex-volume identity $\int_{\Delta^k} dt = |t|^k/k!$. The support and evolution layer is reusable for any lattice-system result. Contributions that prove the milestones in order, or that develop the support calculus independently, are welcome.

Selected references

• J. Haah, M. B. Hastings, R. Kothari, G. H. Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM J. Comput. (2021); arXiv:1801.03922v4 (2020). https://arxiv.org/abs/1801.03922
• E. H. Lieb, D. W. Robinson, The finite group velocity of quantum spin systems, Comm. Math. Phys. 28 (1972) 251–257. https://doi.org/10.1007/BF01645779
• M. B. Hastings, Lieb–Schultz–Mattis in higher dimensions, Phys. Rev. B 69 (2004) 104431. https://arxiv.org/abs/cond-mat/0305505
• B. Nachtergaele, R. Sims, Lieb–Robinson bounds and the exponential clustering theorem, Comm. Math. Phys. 265 (2006) 119–130. https://arxiv.org/abs/math-ph/0506030
• M. B. Hastings, T. Koma, Spectral gap and exponential decay of correlations, Comm. Math. Phys. 265 (2006) 781–804. https://arxiv.org/abs/math-ph/0507008

Motivation

A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.

The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.

Setting

Let $\Lambda$ be a finite set of sites equipped with a metric $\operatorname{dist}(x,y)$. Each site has the same local Hilbert space $\mathbb C^q$, and the whole system has product basis indexed by configurations $\sigma:\Lambda\to\{0,\ldots,q-1\}$. An operator supported on $X\subseteq\Lambda$ is a matrix of the form $m_X\otimes I_{\Lambda\setminus X}$: it may change the configuration on $X$, but acts as the identity on every site outside $X$. The matrix norm throughout is the spectral operator norm.

For every $X\subseteq\Lambda$, let $h_X$ be a Hermitian operator supported on $X$, and define the time independent Hamiltonian $H=\sum_{X\subseteq\Lambda}h_X$. The sum includes all subsets, including the empty set. Let

$$O(t;J)=e^{iJt}Oe^{-iJt},\qquad O(t)=O(t;H).$$

For site sets, write $X\sim Y$ when $X\cap Y\ne\varnothing$, and $\operatorname{dist}(x,Y)=\min_{y\in Y}\operatorname{dist}(x,y)$ when $Y$ is nonempty. The diameter is $\operatorname{diam}(X)=\max_{x,y\in X}\operatorname{dist}(x,y)$ for nonempty $X$. The paper imposes two quantitative conditions. First, for some $0\le\eta\le1$, every pair of terms has a small commutator:

$$\|[h_X,h_Y]\|\le 2\eta\|h_X\|\|h_Y\|.\tag{14}$$

Second, for some $\zeta,\mu>0$, the interactions decay in the weighted sense

$$\sum_{X\ni x}\|h_X\|\,|X|^2e^{\mu\operatorname{diam}(X)}\le\zeta \qquad(x\in\Lambda).\tag{15}$$

Neither condition bounds each $\|h_X\|$ by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.

Formalization targets

The goal is Lemma 12. For an operator $A$ supported on $X$ and an operator $B$ supported on a disjoint set $Y$, and every real $t$, the proposed formal statement is

$$\|[A(t),B]\|\le \frac{2}{\sqrt\eta}\|A\|\|B\| \bigl(e^{\zeta|t|\sqrt{8\eta}}-1\bigr) \sum_{x\in X}e^{-\mu\operatorname{dist}(x,Y)}. \tag{16}$$

The coefficient of $|t|$ in the exponential is proportional to $\sqrt\eta$. The goal keeps the paper's explicit factor $2/\sqrt\eta$, its $\sqrt{8\eta}$ inside the exponential, and the full sum over sites in $X$. The statement is for $\eta>0$, as the displayed formula is undefined at $\eta=0$; a family satisfying (14) with $\eta=0$ also satisfies it for any positive $\eta\le1$.

The milestones follow the source's numbered displays: the initial estimates for $C_B$ and $D_B$ in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its $k$th line in (37). Here $C_B(X,t)$ takes a supremum over supported operators of norm at most one, and $D_B(X,t)=\|[h_X(t),B]\|$. The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.

Significance

The bound shows that a commutator is small when the support of $B$ is far from $X$, with a rate determined by the decay parameter $\mu$ and the small commutator parameter $\eta$. It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to $\sqrt\eta$ can occur under their hypotheses, so a linear dependence on $\eta$ is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.

Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.

Difficulty

The obvious global norm bound $\|[A(t),B]\|\le2\|A\|\|B\|$ ignores the distance between supports. Merely bounding $\|H\|$ also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.

Formalization scope

Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension $q$ is used at every site; qubits occur at $q=2$. Operators are complex matrices on the configuration space $\Lambda\to\operatorname{Fin}(q)$, with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and $H$ is the sum over all subsets. Time is real and $H$ is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.

The goal explicitly requires $X\cap Y=\varnothing$. The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at $t=0$ while the left side need not be. The positive $\eta$ condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to $t\ge0$, the direction for which the displayed forward integral uses $D_B(Z,s)$ and $C_B(Z\cup X,s)$.

For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. $C_B$ uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the $q=2$ case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at $\eta=0$, a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.

Selected references

• Jeongwan Haah, Matthew B. Hastings, Robin Kothari and Guang Hao Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM Journal on Computing, 2021. arXiv:1801.03922v4, Appendix C.1–C.3, pp. 21–25.

Motivation

The two-dimensional directed polymer is a random walk whose paths are reweighted by a random space-time environment. Its logarithmic partition function is a discrete counterpart of the height field of the two-dimensional Kardar–Parisi–Zhang equation. At the intermediate-disorder scale, the random weighting becomes weaker as the walk grows, yet its fluctuations remain visible. Caravenna, Sun and Zygouras prove that throughout the subcritical regime $0<\hat\beta<1$, spatial averages of the centred log-partition function converge to Gaussian fluctuations described by an additive stochastic heat equation (Theorem 1.6, p. 6).

The polymer formulation matters because it is a concrete finite-path model: each partition function is an average over finitely many nearest-neighbour walks, while its limit retains the effect of disorder at every scale. The same paper treats the continuum KPZ equation separately; this mission takes its stated polymer theorem as the target. Earlier work in dimension $1+1$ studied a different intermediate-disorder scaling and a Wiener-chaos limit (Alberts, Khanin and Quastel, 2014). The two-dimensional result concerns a distinct regime and a different limit.

Setting

Let $S$ be the simple symmetric random walk on $\mathbb Z^2$. Starting at $x$, it chooses each of its four nearest-neighbour steps with probability $1/4$. Write $q_n(z)=P_0(S_n=z)$, and let $\widetilde S$ be an independent copy. Their expected overlap through time $N$ is

$$R_N=\sum_{n=1}^N P(S_n=\widetilde S_n)=\sum_{n=1}^N\sum_{z\in\mathbb Z^2}q_n(z)^2.$$

For a fixed $\hat\beta\in(0,1)$, the disorder strength is $\beta_N=\hat\beta/\sqrt{R_N}$. The environment $\omega(n,z)$ consists of independent, identically distributed real random variables with mean zero, variance one and finite exponential moments at all sufficiently small positive arguments. Its logarithmic moment generating function is $\lambda(b)=\log\mathbb E[e^{b\omega}]$. The law also obeys the paper's concentration assumption (1.20): convex 1-Lipschitz functions of any finite collection of environment variables have stretched-exponential deviations from a median, measured with Euclidean distance (pp. 5–6).

For a length-$N$ walk from $x$, sum $\beta_N\omega(n,S_n)-\lambda(\beta_N)$ over times $1,\ldots,N$, exponentiate, and average over paths. The result is the partition function $Z_N(x)$. Where $\lambda(\beta_N)$ is finite, its centring gives $\mathbb E Z_N(x)=1$. A restricted function $Z_{\Lambda,b}(x)$ samples disorder only from the space-time sites in $\Lambda$. Section 2 uses an early window $A_N^x$ near the start and a late window $B_N^{\ge}$ to define $Z_N^A(x)$, its remainder $\widehat Z_N^A(x)=Z_N(x)-Z_N^A(x)$, and $Z_N^{B\ge}(x)$ (pp. 7–9).

At macroscopic time $t>0$ and position $y\in\mathbb R^2$, the fluctuation field is

$$\mathfrak h_N(t,y)=\frac{\log Z_{\lfloor tN\rfloor}(\lfloor\sqrt N y\rfloor)-\mathbb E[\log Z_{\lfloor tN\rfloor}(0)]}{\beta_N}.$$

The floor of a vector is componentwise. In the numerator, $Z_{\lfloor tN\rfloor}$ uses the disorder strength $\beta_{\lfloor tN\rfloor}$; the field is divided by $\beta_N$, exactly as in (1.23).

Formalization targets

For every $t>0$ and smooth compactly supported test function $\phi$, Theorem 1.6 asserts

$$\int_{\mathbb R^2}\mathfrak h_N(t,y)\phi(y)\,dy\xrightarrow{d}\langle v^{(\sqrt2c_{\hat\beta})}(t/2,\cdot),\phi\rangle,\qquad c_{\hat\beta}=\sqrt{\frac1{1-\hat\beta^2}}.$$

The tested limit is centred Gaussian. Its variance is $(\sqrt2c_{\hat\beta})^2\sigma_\phi^2(t/2)$, where

$$\sigma_\phi^2(s)=\iint\phi(x)K_s(x,y)\phi(y)\,dx\,dy,\qquad K_s(x,y)=\int_0^s\frac{e^{-|x-y|^2/(4u)}}{4\pi u}\,du.$$

The milestone list follows the paper's stated results: second-moment bounds (3.2)–(3.4), higher moments for some $p>2$ (3.12), a left-tail bound (Proposition 3.1) and the negative and logarithmic moments it yields (3.14)–(3.16), vanishing spatial averages for two error terms (Propositions 2.1–2.2), replacement by the late-window term (Proposition 2.3), and the Gaussian limit for that term (Proposition 2.4). These are the exact result labels used in Sections 2 and 3 (pp. 8–13).

Significance

The theorem identifies the fluctuation law of the logarithm of the polymer partition function for every $\hat\beta$ strictly below the critical value $1$. The coefficient $c_{\hat\beta}$ records the disorder strength in the limiting covariance, and the time $t/2$ reflects the two-dimensional walk's covariance convention. Without the spatial averaging and normalization, the statement would concern a different observable; the theorem characterizes a field tested against compactly supported functions (Theorem 1.6 and Remark 1.7).

The result is proved in the cited paper. This mission asks for a machine-checked proof of that known result and its curated supporting statements. The reusable output includes a finite-path polymer model on $\mathbb Z^2$, a precise restricted partition function, the disorder concentration assumption, and the Gaussian covariance functional. The published atomic polymer model already supplies the space-time cells, steps, walk positions and log moment generating function; this mission extends that common base to the centred, spatially shifted model of this paper.

Difficulty

Pointwise size does not identify the limiting spatial fluctuations. The early-window partition function captures much of $Z_N(x)$ at a fixed site, yet its averaged logarithm vanishes at the target scale. The small remainder cannot simply be discarded: after division by the early-window function, its late-time component carries the Gaussian limit. The paper separates these effects in Propositions 2.1–2.4 and needs moment and left-tail control to keep the logarithmic expression meaningful (Sections 2–4). A direct Taylor expansion of $\log Z_N$ around its mean would lose this distinction.

Formalization scope

Lean uses finite sequences of four-neighbour steps and the Euclidean norm on $\mathbb R^2$. Disorder is a family indexed by positive walk times and lattice sites; the time-zero row of its ambient type is unused. The full and restricted partition functions are finite walk averages. The concentration assumption quantifies over Euclidean 1-Lipschitz convex functions and their medians. The test class of Theorem 1.6 is $C_c^\infty(\mathbb R^2)$; the four Section 2 propositions use $C_c(\mathbb R^2)$. Treating “smooth” as analytic would make compactly supported tests trivial, so the Lean statement uses the smooth differentiability order.

The target additive stochastic heat observable is represented by its Gaussian law and the kernel above; the random field $v^{(c)}$ itself is not formalized, and the statement does not need it. The kernel takes extended nonnegative values because it is infinite on the diagonal; the diagonal has zero area in the tested covariance integral. Moments and $L^1/L^2$ convergence use extended nonnegative integrals. The paper assumes exponential moments only near zero, so bounds whose printed form quantifies over every $N$ are stated for all sufficiently large $N$, avoiding default values of the logarithmic moment generating function at early indices. The spatial sums have finite support because the test functions do. Replacing the Euclidean norm by the sup norm would change the early window (a square instead of a disc), the kernel and the class of 1-Lipschitz functions in (1.20), so all of these are Euclidean. The polymer propositions are stated for every window exponent below a threshold, as in (2.2), and the passage from the time-1 lattice averages of Propositions 2.1–2.4 to the general-time integral of Theorem 1.6 is part of the proof work, not of the statements. Contributions to the polymer moments, left-tail estimate, replacement propositions and Gaussian limit all feed the stated goal.

Selected references

• Francesco Caravenna, Rongfeng Sun and Nikos Zygouras, The two-dimensional KPZ equation in the entire subcritical regime, Annals of Probability 48(3), 2020; formalization source: arXiv:1812.03911v3.
• Tom Alberts, Konstantin Khanin and Jeremy Quastel, The intermediate disorder regime for directed polymers in dimension 1+1, Annals of Probability 42(3), 2014, DOI:10.1214/13-AOP895.

Motivation

A directed polymer in random environment is a random walk path reweighted by a random potential that is refreshed at every time step. It is a basic model of a one-dimensional object (a polymer, an interface, a flux line) pinned by impurities, and a discrete version of the KPZ universality class in dimension $1+1$. A central question is localization: whether the walk's endpoint at time $n$, under the random Gibbs measure, concentrates on a few sites or spreads out like a simple random walk.

For a fixed disorder law there is a critical inverse temperature $\beta_c$ (Comets–Yoshida, Ann. Probab. 2006). In the low-temperature phase $\beta>\beta_c$ the endpoint has atoms of positive mass, in the Cesàro sense, at a positive fraction of times (Carmona–Hu 2002, Comets–Shiga–Yoshida 2003); in the high-temperature phase it does not. Atoms alone say nothing about geometry: the mass could sit on a few sites that are far apart. Bates and Chatterjee (arXiv:1612.03443v5, Ann. Probab. 2020) prove that in the low-temperature phase the mass also sits on a region of bounded diameter at a positive fraction of times, in every dimension and for every disorder law with exponential moments. Before this, geometric localization was known only for the integrable log-gamma polymer in $1+1$ dimensions (Comets–Nguyen 2016).

Setting

Fix $d\ge1$. Let $(X_u)_{u\in\mathbb N\times\mathbb Z^d}$ be i.i.d. real random variables with law $\mathfrak L$, not supported on a single point, such that $\lambda(\alpha)=\log\mathbf E\,e^{\alpha X_u}<\infty$ for $\alpha\in[-2\beta,2\beta]$ (assumption (1.1)), where $\beta\ge0$ is the inverse temperature. For a nearest-neighbour path $\gamma$ of length $n$ from the origin, its weight is $\exp(\beta\sum_{i=1}^n X_{i,\gamma(i)})$. The endpoint distribution $f_n(x)=\rho_n(\omega_n=x)$ is the total weight of paths ending at $x$ divided by the total weight of all $(2d)^n$ paths. The partition function is $Z_n=(2d)^{-n}\sum_\gamma\exp(\beta\sum_{i=1}^nX_{i,\gamma(i)})$ and the free energy is $F_n=\frac1n\log Z_n$. The limit $p(\beta)=\lim\mathbf E F_n$ exists, and $\beta_c$ is characterised by $p(\beta)=\lambda(\beta)$ for $0\le\beta\le\beta_c$ and $p(\beta)<\lambda(\beta)$ for $\beta>\beta_c$.

For $\delta>0$ and $K\ge0$ let $\mathcal G_{\delta,K}$ be the set of probability mass functions on $\mathbb Z^d$ that give mass greater than $1-\delta$ to some set $D$ with $\operatorname{diam}(D)=\sup_{x,y\in D}\|x-y\|_1\le K$.

The proofs work on the space $\mathcal S$ of partitioned subprobability measures: functions $f\ge0$ on $\mathbb N\times\mathbb Z^d$ with $\sum f\le1$, modulo translations of each copy of $\mathbb Z^d$, with a metric $d$ that makes $\mathcal S$ compact. The update $f_n\mapsto f_{n+1}$ induces a Markov kernel $\mathcal T$ on $\mathcal S$; $\mathcal K$ is its set of invariant probability measures and $\mathcal M\subset\mathcal K$ the minimisers of a free-energy functional $\mathcal R$. On $\mathcal S$ the mission uses the functionals $\max(f)=\max_uf(u)$, the support number $N(f)$ (number of copies carrying mass), $W_\delta(f)$ (the least diameter of a region of one copy with mass $>1-\delta$), $m(f)=\max_nq_n(f)$ and $Q(f)=\sum_nq_n(f)/(1-q_n(f))$, where $q_n(f)$ is the mass of copy $n$.

Formalization targets

Goal: Theorem 1.2 (= Theorem 7.3(a),(c))

If $\beta>\beta_c$, then for every $\delta>0$ there are $K<\infty$ and $\theta>0$, depending only on $\delta,\mathfrak L,\beta,d$, such that

$$\liminf_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}\ge\theta\quad\text{a.s.}$$

If $0\le\beta\le\beta_c$, then for every $K$ and every $\delta\in(0,1)$,

$$\lim_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}=0\quad\text{a.s.}$$

The goal fixes no constants: $K$ and $\theta$ are only asserted to exist.

Milestones

1. Lemma 5.4: $\max$ is continuous on $\mathcal S$.
2. Theorem 5.3: the Cesàro average of $\max_xf_i(x)$ tends to $0$ a.s. at high temperature and has $\liminf\ge c>0$ a.s. at low temperature.
3. Lemma 7.1: $W_\delta$ is upper semicontinuous; $m$ and $Q$ are lower semicontinuous.
4. Lemma 7.2: at low temperature $\int Q\,d\nu=\infty$ for every $\nu\in\mathcal M$.
5. Theorem 7.3(b): under the single-copy condition $\nu(N=1)=1$ for all $\nu\in\mathcal M$ (7.4), localization holds with full density $\theta\ge1-\delta$.
6. Proposition 7.4: under (7.4), $\lim_{K\to\infty}\liminf_n\frac1n\sum_{i<n}\rho_i(\omega_i\in\mathcal C_i^K)=1$ a.s., where $\mathcal C_i^K$ is the set of sites within distance $K$ of every mode of $f_i$.

Significance

The theorem shows that the low-temperature phase is detected by the shape of the endpoint distribution, not only by its largest atom: positive-density geometric localization holds if and only if $\beta>\beta_c$. The determinism of $K$ and $\theta$ makes the statement uniform over all environments with the given law. The conditional results 5 and 6 reduce full-density and favourite-region localization to a single property of the limit set $\mathcal M$, which is open.

The result is proved on paper; nothing in it is machine-checked. A formalization would produce a checked development of the compact space $\mathcal S$, of the Markov kernel $\mathcal T$, and of the variational characterisation of the free energy, which also underlies the companion mission on asymptotic pure atomicity of the same paper.

Difficulty

The obvious approach, tracking $f_n$ in $\ell^1(\mathbb Z^d)$, fails because mass escapes to infinity: the sequence $(f_n)$ has no convergent subsequence in any space of probability measures on $\mathbb Z^d$. The paper's compactification keeps pieces of mass that drift apart as separate copies, so a limit point can split one copy's mass over several. The semicontinuity of $W_\delta$, $m$ and $Q$ (Lemma 7.1) only goes one way for this reason, and positivity of the localized fraction needs the separate identity of Lemma 7.2, which uses strict convexity and the non-degeneracy of $\mathfrak L$. Theorem 5.3 already requires the full variational machinery of §4 (convergence of empirical measures to $\mathcal M$), which is the companion mission's subject.

Formalization scope

Points are $\mathbb Z^d=$ Fin d → ℤ, cells are ℕ × (Fin d → ℤ), and paths are sequences of $n$ signed coordinate steps. The environment is a family of independent measurable random variables, each with law $\mathfrak L$, on an arbitrary probability space. The phases are encoded through Theorem A as $\lim\mathbf E F_n<\lambda(\beta)$ ($\beta>\beta_c$) and $\lim\mathbf EF_n=\lambda(\beta)$ ($0\le\beta\le\beta_c$), with $\mathbf EF_n$ computed under the canonical product environment. Elements of $\mathcal S$ are represented by their representatives, with the topology generated by $d$-balls (no quotient). In the goal, $K$ and $\theta$ are chosen before the probability space. Part (a) is stated for all $\delta>0$ and part (c) for $\delta\in(0,1)$, as printed.

Trivializing encodings are ruled out: $\mathcal G_{\delta,K}$ requires total mass exactly $1$; $W_\delta$ and $N$ take values in $\mathbb N\cup\{\infty\}$ so that an empty infimum is $\infty$; $Q$ is computed in $[0,\infty]$ so that $1/0=\infty$; the sum in $\widetilde F$ is taken in $[0,\infty]$; $\mathcal M$ avoids a real infimum over $\mathcal K$; $\mathfrak L$ is non-degenerate; and the phase hypotheses are limits that exist.

A complete development needs: the metric space $(\mathcal S,d)$ and its compactness, the measurability and continuity of $\mathcal T$, the Wasserstein space $\mathcal P(\mathcal S)$ (here through the published RWPI.SqrtLasso.transportCost), and the convergence $\mathcal W(\mu_n,\mathcal M)\to0$ (Theorem 4.9) together with $\mathcal M=\{\delta_0\}$ at high temperature (Theorem 5.2), both posed in the companion mission. Contributions to any milestone, and to the shared infrastructure of $\mathcal S$, are welcome.

Selected references

• E. Bates, S. Chatterjee, The endpoint distribution of directed polymers, Ann. Probab. 48 (2020); arXiv:1612.03443v5. https://arxiv.org/abs/1612.03443
• F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006). https://doi.org/10.1214/009117905000000828
• F. Comets, T. Shiga, N. Yoshida, Directed polymers in a random environment: path localization and strong disorder, Bernoulli 9 (2003). https://doi.org/10.3150/bj/1065444233
• P. Carmona, Y. Hu, On the partition function of a directed polymer in a Gaussian random environment, Probab. Theory Related Fields 124 (2002). https://doi.org/10.1007/s004400200213
• F. Comets, V.-L. Nguyen, Localization in log-gamma polymers with boundaries, Probab. Theory Related Fields 166 (2016). https://doi.org/10.1007/s00440-015-0662-4
• F. Comets, Directed Polymers in Random Environments, Lecture Notes in Math. 2175, Springer (2017). https://doi.org/10.1007/978-3-319-50487-2

Motivation

Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.

Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).

Setting

An operational-probabilistic theory (OPT) has systems $A,B,\dots$, a composite system $AB$ for every pair, and, for each pair $(A,B)$, tests: finite families $\{\mathcal C_i\}_{i\in X}$ of transformations from $A$ to $B$. Tests with no input are preparation tests (families of states $\rho_i$), tests with no output are observation tests (families of effects $a_j$). Composing a preparation test with an observation test yields a joint probability distribution $p(i,j)=(a_j|\rho_i)$, and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of $A$ span a real vector space $\mathrm{St}_{\mathbb R}(A)$ of finite dimension $D_A$, effects are linear functionals on it, and transformations are linear maps. $\mathrm{St}_1(A)$ denotes the normalized (deterministic) states.

Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face $F_\rho$ of a state, and perfectly distinguishable families $\{\rho_i\}_{i=1}^N$ (there is an observation test with $(a_j|\rho_i)=\delta_{ij}$). The informational dimension $d_A$ is the common size of all maximal perfectly distinguishable families of pure states.

Formalization targets

Goal (Theorem 20)

For every theory satisfying the six principles and every system $A$, there is a real-linear isomorphism $S:\mathrm{St}_{\mathbb R}(A)\to\mathrm{Herm}_n(\mathbb C)$ with

$$S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq 0,\ \operatorname{tr}M=1\},$$

and $n=d_A$, the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on $\mathbb C^{d_A}$.

Milestones

In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 ($d_{AB}=d_Ad_B$), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 ($D_A=d_A^2$), Theorem 13 (the Bloch ball and $G_A\cong SO(3)$ for $d_A=2$), Theorem 16 (superposition principle).

Significance

The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula $D_A=d_A^2$ (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.

The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.

Difficulty

The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of $O(3)$), then projections on faces, the superposition principle and finally a coordinate system on $d$-level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.

Formalization scope

Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: $\mathrm{St}_{\mathbb R}(A)$ is modelled as $\mathbb R^{D_A}$, effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.

Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.

Selected references

• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311 (2011). https://doi.org/10.1103/PhysRevA.84.012311
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Probabilistic theories with purification, Phys. Rev. A 81, 062348 (2010). https://doi.org/10.1103/PhysRevA.81.062348
• L. Hardy, Quantum theory from five reasonable axioms (2001). https://arxiv.org/abs/quant-ph/0101012
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001 (2011). https://arxiv.org/abs/1004.1483

Motivation

A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order $N$, the free energy fluctuates on the scale $N^{1/3}$ and the path wanders on the scale $N^{2/3}$. For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).

For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order $N^{2/3}$ in the characteristic direction. The model has since become a basic exactly solvable polymer:

• 2009: Seppäläinen, the log-gamma polymer with boundary conditions; variance bounds of order $N^{2/3}$ and path fluctuation exponent $2/3$, by a Burke property and a variance identity.
• 2013: Borodin, Corwin and Remenik, Fredholm determinant formula and Tracy–Widom GUE limit of the free energy, for a range of parameters.
• 2014: Corwin, O'Connell, Seppäläinen and Zygouras, Tropical combinatorics and Whittaker functions, an exact formula for the law of the partition function via the geometric RSK correspondence.

The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.

Setting

Sites are $\mathbb Z_+^2=\{0,1,2,\dots\}^2$ and $\mathbb N=\{1,2,\dots\}$. A weight configuration assigns a positive number $Y_{i,j}$ to each site. On the axes, $U_{i,0}=Y_{i,0}$ and $V_{0,j}=Y_{0,j}$ for $i,j\in\mathbb N$ are the boundary weights, and $Y_{i,j}$, $i,j\in\mathbb N$, are the bulk weights.

An up-right path from $(0,0)$ to $(m,n)$ is a sequence $x_0=(0,0),x_1,\dots,x_{m+n}=(m,n)$ whose steps are $(1,0)$ or $(0,1)$. The partition function is

$$Z_{m,n}=\sum_{x}\prod_{k=1}^{m+n}Y_{x_k},$$

the weight of the origin excluded, $Z_{0,0}=1$. The quenched polymer measure gives the path $x$ probability $Q^\omega_{m,n}(x)=Z_{m,n}^{-1}\prod_{k=1}^{m+n}Y_{x_k}$, and the annealed measure is its average $P_{m,n}=\mathbb E\,Q^\omega_{m,n}$ over the environment. The exit points $\xi_x$ and $\xi_y$ are the numbers of initial steps the path takes along the $x$-axis and along the $y$-axis.

Assumption (2.4). Fix $0<\theta<\mu$. The weights $\{U_{i,0},V_{0,j},Y_{i,j}: i,j\in\mathbb N\}$ are independent with

$$U_{i,0}^{-1}\sim\mathrm{Gamma}(\theta,1),\qquad V_{0,j}^{-1}\sim\mathrm{Gamma}(\mu-\theta,1),\qquad Y_{i,j}^{-1}\sim\mathrm{Gamma}(\mu,1).$$

Let $\Psi_0=(\log\Gamma)'$ and $\Psi_1=\Psi_0'$ be the digamma and trigamma functions. The characteristic direction is $(\Psi_1(\mu-\theta),\Psi_1(\theta))$. For a real scaling parameter $N$ and a constant $\gamma$, the endpoint satisfies

$$|m-N\Psi_1(\mu-\theta)|\le\gamma N^{2/3}\quad\text{and}\quad|n-N\Psi_1(\theta)|\le\gamma N^{2/3}\qquad(2.6).$$

Formalization targets

Goal: Theorem 2.1

There are constants $0<C_1,C_2<\infty$ and $N_0$, depending on $\theta,\mu,\gamma$, such that under (2.4) and (2.6)

$$\mathrm{Var}(\log Z_{m,n})\le C_2N^{2/3}\quad(N\ge1),\qquad C_1N^{2/3}\le\mathrm{Var}(\log Z_{m,n})\quad(N\ge N_0).$$

Milestones

The upper bound runs through the Burke property and the variance identity:

• Lemma 3.1 (monotonicity of the recursion (3.2)), Lemma 3.2 (gamma reversibility), Theorem 3.3 (Burke property), the mean (2.5), $\mathbb E\log Z_{m,n}=-m\Psi_0(\theta)-n\Psi_0(\mu-\theta)$.
• Theorem 3.7, the variance identity

$$\mathrm{Var}[\log Z_{m,n}]=n\Psi_1(\mu-\theta)-m\Psi_1(\theta)+2E_{m,n}\Bigl[\sum_{i=1}^{\xi_x}L(\theta,Y_{i,0}^{-1})\Bigr].$$

• Lemma 4.1 (variance comparison in $\theta$), Lemma 4.2, the exit-point bound (4.32) $E(\xi_x)\le CN^{2/3}$, Lemma 4.3 (quenched exit-point tails).

The lower bound runs through partition-function comparisons:

• Lemma 5.1, Lemma 5.4 (coupling), Lemma 5.5(i), Proposition 5.3 ($\lim_{\delta\searrow0}\varlimsup_NP\{1\le\xi_x\le\delta N^{2/3}\}=0$), Corollary 5.6 ($\mathrm{Var}\ge cN^{2/3}$, $c>0$).

Significance

The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent $1/3$ for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for $N^{-1}\log Z_{m,n}$ (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent $2/3$ (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).

Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.

Difficulty

The obvious route to a variance bound, a martingale decomposition of $\log Z_{m,n}$ over the $mn$ independent weights, gives only $\mathrm{Var}=O(m+n)$, i.e. order $N$; it cannot see the cancellation that produces $N^{2/3}$. The order $N^{2/3}$ is specific to the characteristic direction: off it, $\log Z_{m,n}$ satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters $\theta,\mu-\theta$ and the endpoint $(m,n)$. The upper bound requires controlling the annealed exit point $E(\xi_x)$ at the scale $N^{2/3}$, with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance $o(N^{2/3})$ from the origin with non-vanishing probability, which no upper-bound estimate implies.

Formalization scope

Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.

• Sites are ℕ × ℕ; a path is a step sequence with a fixed number of east steps; $Z$ is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under $y\mapsto y^{-1}$ equal to Mathlib's gammaMeasure (shape, rate $1$). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.
• $N$ is real and $N^{2/3}$ is a real power. Variances use Mathlib's variance, and every upper bound or identity also asserts $\log Z_{m,n}\in L^2$ (or integrability of the averaged quantity), so that the junk value $0$ of variance and of the Bochner integral cannot satisfy it.
• Constants come after the parameters $(\theta,\mu,\gamma)$ and before the probability space (universe Type), the environment, $N$ and $(m,n)$. Upper limits in $N$ are stated as "for every $\eta>0$ there is $N_0$ with the bound $+\eta$ for $N\ge N_0$". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.
• Corrected slips. (i) Theorem 2.1 prints the lower bound for all $N\ge1$. It fails at $N=1$, $\theta=1$, $\mu=2$, $\gamma=2$ with $(m,n)=(0,0)$, where the variance is $0$. The lower bound is stated for $N\ge N_0$, which is what Corollary 5.6 proves. (ii) The "only if" of Lemma 3.2 fails for the constants $U=V=1$, $Y=1/2$. The hypothesis "$U$ is not a.s. constant" is added. (iii) Corollary 5.6 states $c>0$ explicitly.
• Theorem 3.3 is stated for down-right paths that coincide with the axes outside a finite portion. The paper reduces the general case to these.
• Not included: Lemma 3.5 (reversal), Proposition 3.4, Lemma 5.5(ii).

A formalization in which $Z$ includes the origin's weight, the laws are not exactly the inverse gammas with shapes $\theta,\mu-\theta,\mu$ and rate $1$, independence is dropped, $C_1=0$ is allowed, or the constants depend on the environment or on $N$ does not state Theorem 2.1.

Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.

Selected references

• T. Seppäläinen, Scaling for a one-dimensional directed polymer with boundary conditions, Ann. Probab. 40 (2012) 19–73; revised version arXiv:0911.2446v4. https://arxiv.org/abs/0911.2446
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000) 437–476. https://arxiv.org/abs/math/9903134
• M. Balázs, E. Cator, T. Seppäläinen, Cube root fluctuations for the corner growth model associated to the exclusion process, Electron. J. Probab. 11 (2006) 1094–1132. https://arxiv.org/abs/math/0603306
• I. Corwin, N. O'Connell, T. Seppäläinen, N. Zygouras, Tropical combinatorics and Whittaker functions, Duke Math. J. 163 (2014) 513–563. https://arxiv.org/abs/1110.3489
• A. Borodin, I. Corwin, D. Remenik, Log-gamma polymer free energy fluctuations via a Fredholm determinant identity, Comm. Math. Phys. 324 (2013) 215–232. https://arxiv.org/abs/1206.4573
• E. Lukacs, A characterization of the gamma distribution, Ann. Math. Statist. 26 (1955) 319–324. https://doi.org/10.1214/aoms/1177728549

Motivation

Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.

Setting

The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.

Formalization target

The selected goal is OAI.MinimalVertex.main. Its central assertion is

$$\mathrm{energy\ bounds}\ \land\ \mathrm{strong\ locality}\ \land\ \mathrm{irreducible\ conformal\ net}.$$

The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.

Significance and status

The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Strongly rational unitary vertex operator algebras and conformal nets, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.

Setting

At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.

Formalization target

The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is

$$\frac1{25}\operatorname{dist}(\psi,\mathbb C\Psi_{\rm L})^2\leq E(\psi).$$

The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.

Significance and status

The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.Laughlin.mainTarget_proved (Open).
• OAI.LaughlinFock.thm_fock (Open).
• OAI.Laughlin.planar_gap (Open).

Selected references

• OpenAI, A Fock-space inequality and the Laughlin spectral gap, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

An exterior electron count defines a radius of a neutral atom without selecting individual electrons. Its scaling tests how well Thomas–Fermi theory describes the outer region of the full interacting atom. The pinned manuscript supplies the research context.

Setting

Choose any normalized ground state for each neutral atom with N+1 electrons. The radius is the infimum of radii outside which the expected electron mass is at most m.

Formalization target

The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is

$$m^{1/3}R_m^{\rm upper},\ m^{1/3}R_m^{\rm lower}\longrightarrow (81\pi^2/2)^{1/3}.$$

The theorem states that, for every choice of wavefunctions Ψ_N for neutral atoms with N+1 electrons and nuclear charge Z=N+1 (each a spin-dependent complex function of N+1 positions in three-dimensional space, with spins taking two values), such that each Ψ_N is a normalized ground state, the outer radii of the atoms obey a Thomas–Fermi-type scaling law. A normalized ground state is an antisymmetric wavefunction with a weak gradient, square-integrable in each spin component together with its gradient, with finite Coulomb integrals against |Ψ|², total squared norm 1 summed over spins, and minimal energy among all such normalized functions. The energy is half the squared L² norm of the gradient plus the expectation of the Coulomb potential, which is −Z times the sum of inverse distances of electrons to the nucleus plus the sum of inverse inter-electron distances over pairs. The electron density is N+1 times the spin-summed integral of |Ψ|² over the other N positions, and the radius for m is the infimum of r≥0 such that the density mass outside the ball of radius r is at most m. For each m, upperRadius and lowerRadius are the limsup and liminf, in the extended reals, of these radii as N→∞ with N+1>m. With bTF=(81π²/2)^(1/3), the theorem states that both m^(1/3)·upperRadius(m) and m^(1/3)·lowerRadius(m) converge to bTF as m→∞ through the natural numbers.

Significance and status

The target uses extended-real upper and lower radii, followed by a natural-number limit in m. No spherical symmetry is assumed, and the atom remains neutral. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The assertion must hold for every choice of ground states. The inner large-charge limsup and liminf cannot be silently replaced with an assumed pointwise limit.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Generalized outer-electron radii of neutral Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Removing outer electrons changes an atom's energy on a smaller scale than its total binding energy. A total-energy asymptotic alone does not determine the difference. The pinned manuscript supplies the research context.

Setting

The quantum model uses antisymmetric spin-dependent wavefunctions, two spin states, weak gradients and the full nuclear and electron-electron Coulomb interactions. The comparison is with the Thomas–Fermi density functional.

Formalization target

The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is

$$I(m,Z)/m^{7/3}\longrightarrow a,\qquad m\to\infty,\ Z/m\to\infty.$$

The theorem states that the proposition MainStatement holds: there is a real constant a>0 such that three asymptotic statements about atomic ionization energies all hold with this same a. Here the quantum energy of N electrons around a nucleus of charge Z is the infimum, taken over admissible spin-dependent wavefunctions on (ℝ³)^N, of the energy (1/2) times the total squared L² norm of all gradient components, minus Z times the expectation of Σᵢ 1/|xᵢ|, plus the expectation of Σ_{i<j} 1/|xᵢ−xⱼ|, with energy defined as 0 when N=0. Admissibility means that each spin component and each prescribed gradient component is square integrable, the gradient components are the weak partial derivatives of the values, the values are antisymmetric under simultaneous permutation of spins and positions (by the sign of the permutation, almost everywhere), the total squared norm summed over spins is 1, and the nuclear and electron-electron Coulomb densities are integrable. The ionization energy of removing m electrons from a neutral atom of charge Z is ionization(m,Z)=E(Z, Z−m)−E(Z, Z), with natural-number subtraction. The Thomas-Fermi energy tfEnergy(Z,M) is the infimum over nonnegative integrable densities ρ on ℝ³ of total mass M, with ρ^{5/3}, ρ/|x| and ρ(x)ρ(y)/|x−y| integrable, of (3/10)(3π²)^{2/3}∫ρ^{5/3} − Z∫ρ/|x| + (1/2)∬ρ(x)ρ(y)/|x−y|, and tfIonization(m,Z)=tfEnergy(Z,Z−m)−tfEnergy(Z,Z) for real m and Z. The three conclusions are: for every real m>0, tfIonization(m,Z) tends to a·m^{7/3} as the real number Z tends to infinity; for all natural-number sequences m_j, Z_j with 1≤m_j<Z_j, m_j→∞ and Z_j/m_j→∞, the ratio ionization(m_j,Z_j)/m_j^{7/3} tends to a; and as m→∞ through the naturals, both limsup and liminf over Z of ionization(m,Z), each divided by m^{7/3}, tend to a.

Significance and status

The main proposition includes a positive common constant, the fixed-m Thomas–Fermi limit, the joint quantum limit, and normalized limsup and liminf limits. It concerns energies rather than outer-electron radii. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Errors negligible relative to the total atomic energy can still dominate ionization energies. The common leading constant must work in the joint regime and both iterated limits.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Generalized ionization energies for full Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.

Setting

A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum $(E,P)$, assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.

Formalization targets

$$g_R\ge(1-\varepsilon(R))g,\quad\varepsilon(R)\to0,\quad m_{\mathrm{ADM}}(g_R)=\sqrt{E^2-|P|^2}+\eta_R,\quad0\le\eta_R\le2R^{-1/2}.$$

For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).

The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• schwarzschild equality examples.

Significance

The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.

Formalization scope

The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.

The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.

Formalization targets

$$\mathbb E P_N(\beta)\to\mathcal V_\beta,\qquad P_N(\beta)\to\mathcal V_\beta\ \text{almost surely}\qquad(\beta>0).$$

For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.

The goal is OAI.InvariantIsing.positive_temperature_pressure_unconditional. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• gaussianPattern ground limit unconditional.
• gaussianPattern norm limits unconditional.
• gaussianPattern pressure limit unconditional.
• ground state limit unconditional.
• limiting pressure of extreme limits unconditional.
• limiting wasserstein field pressure of extreme limits unconditional.
• random field pressure tendsto ae unconditional.
• random pressure limit unconditional.
• random pressure tendsto ae unconditional.
• random pressure tendsto in measure unconditional.

Significance

The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.

Formalization scope

The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by $\beta$. The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.

The shared definitions are supplied by InvariantIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The spherical perceptron assigns random rewards to vectors of fixed length. The source asks for an exact pressure formula without a convexity or symmetry condition on the single-pattern potential. The source is OpenAI's September 2026 manuscript.

Setting

Configurations lie on the sphere of radius $\sqrt n$, equipped with uniform probability measure. There are $\lfloor\alpha n\rfloor$ independent Gaussian patterns. The variational value minimizes a Brownian stochastic-control functional plus an extended nonnegative entropy over monotone trials.

Formalization targets

$$\exists p\in\mathbb R:\quad\mathcal V(\alpha,\beta,\varphi)=p,\qquad\mathbb E p_n\to p,\qquad p_n\xrightarrow{\mathbb P}p.$$

For a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.

The goal is OAI.SphericalPerceptronFreeEnergy.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• spherical linear field formula.

Significance

The selected main target proves finiteness of the variational value, convergence of expected pressure, and concentration around the same number. The linear-field formula is attached as a supporting result. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

An infimum involving a possibly infinite entropy must be connected with the actual finite-dimensional spherical integral. The potential is only bounded and continuous, so smoothness cannot be assumed.

Formalization scope

Density and inverse temperature are strictly positive. Controls are progressively measurable for the stated Brownian filtration and have finite cost. Dimension is written as $N+1$ to stay positive. The Brownian and cascade-based linear-field definition groups are independent references.

The shared definitions are supplied by PerceptronFreeEnergy, SphericalField. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The free energy of the spherical random perceptron, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.

Setting

An overlap path is an almost-everywhere class on $(0,1)$ with a monotone representative taking values in $[0,1]$. The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.

Formalization targets

$$\alpha\ge0,\quad f\in C_b(\mathbb R)\quad\Longrightarrow\quad\exists p\in\mathbb R:\ \operatorname{variationalValue}(\alpha,f)=p\text{ in }\overline{\mathbb R}.$$

For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.

The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.

Significance

The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.

Formalization scope

The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.

The shared definitions are supplied by IsingFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The free energy of the Ising random perceptron, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.