Mathematical Physics

Motivation

A coincident pair of a D-brane and an anti-D-brane in type II string theory carries an open-string tachyon, a mode of negative mass squared. In Sen, hep-th/9805019 it was conjectured that at the minimum of the tachyon potential the negative potential energy exactly cancels the sum of the tensions of the brane and the anti-brane, so that the system decays to a configuration of zero energy density, i.e. the supersymmetric vacuum. The paper formalized here, A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012, gives a short argument for this, and the author says explicitly that it is not a rigorous mathematical proof. The argument follows Gava–Narain–Sarmadi, hep-th/9704006 and belongs to the programme of tachyon condensation. Later work, starting with open string field theory computations, tested the same conjecture numerically.

Setting

Work in string units ($\alpha'=1$). Wrap a D2-brane and an anti-D2-brane on a torus $T^2=S^1\times S^1$ with radii $R_1,R_2$ and area $V=4\pi^2R_1R_2$. Each brane carries one unit of magnetic flux, $F_{12}=2\pi/V$, with signs chosen so that each carries $+1$ unit of D0-brane charge. T-duality on both circles gives a dual torus with radii $\tilde R_i=1/R_i$ and coupling $\tilde g=g/(R_1R_2)$. On the dual torus the system is described by a $U(2)$ gauge theory: a gauge field is a pair $A=(A_1,A_2)$ of $2\times2$ complex-matrix-valued functions of $x=(x^1,x^2)$, with field strength $F_{12}=\partial_1A_2-\partial_2A_1-i[A_1,A_2]$. The gauge transform by a matrix-valued $\Omega$ is $(\Omega\circ A)_\mu=\Omega A_\mu\Omega^{-1}-i(\partial_\mu\Omega)\Omega^{-1}$. The background configuration is

$$A_1=0,\qquad A_2=\frac{2\pi x^1\sigma_3}{\tilde V},\qquad \tilde V=4\pi^2\tilde R_1\tilde R_2,$$

subject to twisted boundary conditions with transition functions $\Omega_1=\exp(ix^2\sigma_3/\tilde R_2)$ and $\Omega_2=1$. A D-brane with coupling $g$ has tension $1/(4\pi^2g)$.

Formalization targets

Goal

With $M(R_1,R_2,g)$ the mass at the classical minimum (two D2-branes with zero field strength on the dual torus, re-expressed through $R_1,R_2,g$), for each fixed $g>0$:

$$\lim_{R_1,R_2\to\infty}\frac{M(R_1,R_2,g)}{4\pi^2R_1R_2}=0 .$$

Milestones (in the paper's order)

1. Eq. (1): $2\pi/(4\pi^2R_1R_2)\to0$ as $R_1,R_2\to\infty$.
2. The background (4) is traceless Hermitian (no $U(1)$ part).
3. Eqs. (5)–(6): the background satisfies the twisted boundary conditions.
4. Eq. (7): $\Omega_2(2\pi\tilde R_1)\Omega_1(0)=\Omega_1(2\pi\tilde R_2)\Omega_2(0)$.
5. The background has field strength $F_{12}=(2\pi/\tilde V)\sigma_3\neq0$.
6. Eq. (8): there is a smooth $SU(2)$-valued $g$ with the boundary behaviour (8).
7. Gauge transformations preserve $F_{12}\equiv0$.
8. Eq. (9): $M=2\tilde R_1\tilde R_2/\tilde g$.
9. Eq. (10): $M=2/g$.
10. Eq. (11): $M/(4\pi^2R_1R_2)=1/(2\pi^2R_1R_2g)$.

Significance

The vanishing of the energy at the tachyon minimum is the basis for identifying stable non-BPS D-branes as tachyonic solitons on brane–antibrane pairs, as discussed at the end of the paper, and it was a starting point for later work on tachyon condensation. The paper's argument is heuristic. This mission makes explicit which steps are mathematics (the gauge-theoretic facts (4)–(8), the gauge covariance used on p. 3, and the algebra (9)–(11) and its limit) and machine-checks them. The physical inputs (the BPS argument that the mass (9) persists as parameters vary, and the identification of the minimum-energy configuration) are recorded as modelling assumptions in the definitions, not proved.

Difficulty

The algebraic milestones (9)–(11) and the limits are elementary. The substantive formal work is in the gauge-theory milestones: computing derivatives of the matrix exponential in (5), the smooth homotopy with flat ends required by (8) (existence rests on the simple connectivity of $SU(2)$, but the statement asks for an explicit smooth $SU(2)$-valued map with prescribed boundary values and vanishing normal derivative), and the covariance computation of the field strength under a non-unitary, merely invertible $\Omega$.

Formalization scope

Coordinates are $x=(x^1,x^2)\in\mathbb R\times\mathbb R$; the paper's index $\mu\in\{1,2\}$ is Fin 2 ($1\mapsto0$, $2\mapsto1$). Matrices are Matrix (Fin 2) (Fin 2) ℂ; partial derivatives are taken entrywise; the inverse is the Mathlib matrix inverse; the exponential is NormedSpace.exp. Radii and couplings are real, with positivity assumed wherever the paper's quantities are physical. The goal cannot be trivialized by division by zero, because it is a statement about the limit of large positive radii. All definitions live in a single definition file under the namespace SenTachyon.

Selected references

• A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012. https://doi.org/10.1088/1126-6708/1998/08/012 (arXiv: https://arxiv.org/abs/hep-th/9805170)
• A. Sen, Stable non-BPS bound states of BPS D-branes, JHEP 08 (1998) 010. https://arxiv.org/abs/hep-th/9805019
• E. Gava, K. S. Narain, M. H. Sarmadi, On the bound states of p- and (p+2)-branes, Nucl. Phys. B 504 (1997) 214. https://arxiv.org/abs/hep-th/9704006
• G. 't Hooft, Some twisted self-dual solutions for the Yang–Mills equations on a hypertorus, Comm. Math. Phys. 81 (1981) 267. https://doi.org/10.1007/BF01208900

Motivation

In the 1993 essay Dimensional Reduction in Quantum Gravity (arXiv:gr-qc/9310026), G. 't Hooft argued that, once gravitational collapse is taken into account, the number of quantum states available to a region of space grows with the area of its boundary rather than with its volume. The essay is the origin of what is now called the holographic principle (developed further by Susskind, arXiv:hep-th/9409089). Besides the physical counting argument, the essay contains a small, fully precise mathematical model: a cellular automaton on the cubic lattice $\mathbb Z^3$ whose data on a one-dimensional line determine the data everywhere. This mission formalizes the quantitative estimates and the automaton statements of the essay.

Setting

Entropy estimates (eqs. (4)–(11)). In natural units, a region bounded by a sphere of radius $R$ has volume $V=\tfrac43\pi R^3$ and area $A=4\pi R^2$. A thermal gas of $Z$ particle species at temperature $T$ has energy $E=C_1 Z V T^4$ and entropy $S=C_2 Z V T^3$ with positive constants $C_1,C_2$. It stays outside its own Schwarzschild radius if $2E<R$. A black hole of mass $M$ has entropy $4\pi M^2$ (eq. (1), additive constant dropped).

Plaquette automaton (eqs. (12)–(19)). Data $f:\mathbb Z^3\to\mathbb Z/p$ live on lattice sites. An elementary plaquette has lowest corner $x$ and is spanned by two of the unit vectors $e^1,e^2,e^3$; its corners in cyclic order are $x,\;x+u,\;x+u+v,\;x+v$. On every plaquette a relation $g(f_1,f_2,f_3,f_4)=0$ is imposed such that any three entries determine the fourth uniquely. The relations may differ from plaquette to plaquette. On the unit cube with corners $A=0$, $B=e^1$, $D=e^2$, $E=e^3$, $C=e^1+e^2$, $F=e^1+e^3$, $H=e^2+e^3$, $G=e^1+e^2+e^3$, the six face relations are (12a–f). The staircase (eq. (14)) is the sequence

$$x(3n+1)=x(3n)+e^1,\qquad x(3n+2)=x(3n+1)-e^2,\qquad x(3n+3)=x(3n+2)+e^3,\qquad n\in\mathbb Z .$$

A family of face relations is consistent (eq. (16)) if every choice of $f(A),f(B),f(D),f(E)$ extends to data on the cube satisfying all six relations; equivalently, the three values of $f(G)$ produced by (12b), (12d), (12f) agree. Linear relations (eq. (17)) have the form $\sum_j a_j f_j+b \equiv 0 \pmod p$, with every $a_j$ invertible mod $p$.

Formalization targets

Goal: the staircase determines everything

For any family of plaquette relations with the three-determine-the-fourth property, two solutions on $\mathbb Z^3$ that agree on the staircase agree everywhere:

$$\Big(\forall n\in\mathbb Z:\ f(x(n))=f'(x(n))\Big)\ \Longrightarrow\ f=f' .$$

Milestones

1. Eqs. (4)–(8): $T<C_3Z^{-1/4}V^{-1/6}$ and $S<C_4Z^{1/4}V^{1/2}=C_5Z^{1/4}A^{3/4}$ for the thermal gas.
2. Eqs. (9)–(11): black holes that fit inside the sphere have total entropy $<A/4$, and $A/4$ is the supremum.
3. Discussion of Fig. 1: on one cube, the data at $D,H,E,F$ determine all eight corners.
4. Eqs. (17)–(19): consistent linear relations with invertible coefficients exist for every modulus $p\ge 2$.
5. Eqs. (14), (17): for the linear relation $f_1-f_2+f_3-f_4\equiv0$, any data on the staircase extend uniquely to a global solution. The staircase data are then exactly the free degrees of freedom.

Significance

The goal is the essay's concrete mathematical example of dimensional reduction: in a $2+1$-dimensional lattice model, a one-dimensional set of data carries all the information. Milestone 5 shows that the reduction is sharp in the linear case: no data beyond the staircase are needed, and none of the staircase data are constrained. Milestones 1–2 are the scaling estimates behind the area law $S_{\max}=A/4$. The physical argument around them (black-hole thermodynamics, the Schwarzschild criterion) is taken as modelling input, not formalized. The results are stated in the essay but, as far as is known, have not been machine-checked.

Difficulty

The local step (one cube, Milestone 3) is elementary. The goal needs a global propagation argument. The staircase is a thin zig-zag line, and each application of a plaquette relation fixes only one new site. So the proof has to show that repeated local determination starting from the line eventually reaches every site of $\mathbb Z^3$, in both directions along the line and in both transverse directions. Layer-by-layer propagation in $t=x_1+x_2+x_3$ does not apply directly, because the staircase is not a full layer.

Formalization scope

Sites are ℤ × ℤ × ℤ. Data take values in ZMod p for an arbitrary natural number $p$; the uniqueness statements hold for every $p$. The three-determine-the-fourth property is stated with unique existence ($\exists!$) for each slot, which matches "uniquely determined" in the essay. Relations may depend on the plaquette, so no translation invariance is assumed. Consistency (16) is encoded as extendability of the four free values on the unit cube. In Milestones 1–2 the region is a round sphere of radius $R$, so $V$ and $A$ are expressions in $R$, and the constants are existentially quantified before all physical variables. Contributions welcome: proofs of each milestone, and further faithful statements from the triangular-lattice model (eqs. (20a–f)).

Selected references

• G. 't Hooft, Dimensional Reduction in Quantum Gravity, essay in honour of A. Salam, 1993. https://arxiv.org/abs/gr-qc/9310026
• L. Susskind, The World as a Hologram, J. Math. Phys. 36 (1995) 6377. https://arxiv.org/abs/hep-th/9409089

Motivation

Neutrinos produced by weak interactions are created in flavour eigenstates ($\nu_e$, $\nu_\mu$, $\nu_\tau$), while they propagate as mass eigenstates. When the two bases differ, the flavour content of a neutrino beam oscillates with distance. In ordinary matter this picture is modified: electron neutrinos scatter coherently forward on electrons via the charged current, which adds an extra potential energy $V_{CC}=\sqrt2\,G_F N_e$ to the $\nu_e$ component only (Wolfenstein 1978). Mikheyev and Smirnov observed that this potential can resonantly enhance the mixing, so that an almost complete flavour conversion is possible even for a tiny vacuum mixing angle — the MSW effect. It is the accepted explanation of the energy dependence of the solar $\nu_e$ deficit and is relevant for neutrinos crossing the Earth and for supernova neutrinos.

This mission formalizes the constant-density result of Section 8.2 of E. Kh. Akhmedov's lecture notes Neutrino physics (hep-ph/0001264): the two-flavour transition probability in matter of constant density, eq. (95), together with the statements that lead to it and follow from it, eqs. (91)–(98).

Setting

Fix the vacuum parameters: the mass-squared difference $\Delta m^2 = m_2^2-m_1^2\in\mathbb R$, the neutrino energy $E>0$, and the vacuum mixing angle $\theta_0\in\mathbb R$. The matter is described by the Fermi constant $G_F$ and the electron number density $N_e$, through the charged-current potential (eq. (87))

$$V_{CC}=\sqrt2\,G_F N_e .$$

Write $a=\Delta m^2/(2E)$. After discarding all terms proportional to the identity (common phases), the vector $\nu(t)=(\nu_e(t),\nu_\mu(t))\in\mathbb C^2$ of flavour amplitudes evolves by the Schrödinger equation $i\,\dot\nu = H\nu$ with the real symmetric MSW Hamiltonian (eq. (91))

$$H=\begin{pmatrix}-\tfrac a2\cos2\theta_0+V_{CC} & \tfrac a2\sin2\theta_0\\[2pt] \tfrac a2\sin2\theta_0 & \tfrac a2\cos2\theta_0\end{pmatrix}.$$

The derived quantities are the energy gap in matter (eq. (94)), the oscillation length in matter (eq. (96)) and the oscillation amplitude in matter (eq. (97)):

$$\Delta_m=\sqrt{(a\cos2\theta_0-V_{CC})^2+a^2\sin^22\theta_0},\qquad l_m=\frac{2\pi}{\Delta_m},\qquad \sin^22\theta=\frac{a^2\sin^22\theta_0}{(a\cos2\theta_0-V_{CC})^2+a^2\sin^22\theta_0}.$$

The vacuum oscillation length is $l_{osc}=4\pi E/\Delta m^2$ (eq. (61)). Distance and time are identified ($L\simeq t$, units with $c=1$).

Formalization targets

Goal — transition probability at constant density (eq. (95))

If $\nu$ solves $i\dot\nu=H\nu$ for all $t$ with $\nu(0)=(1,0)$ (a pure $\nu_e$ is produced at $t=0$), then for every $L$

$$|\nu_\mu(L)|^2=\sin^22\theta\;\sin^2\!\Big(\frac{\pi L}{l_m}\Big).$$

Milestones

1. Common phases are unobservable (Sec. 8.1, below eq. (89)). Adding $c\,\mathbf 1$ ($c\in\mathbb R$) to a Hamiltonian changes a solution only by a phase; multiplying back by $e^{ict}$ gives a solution for the reduced Hamiltonian with the same component moduli.
2. Mixing angle in matter (eq. (93)). There is an angle $\theta$ with $\Delta_m\cos2\theta=a\cos2\theta_0-V_{CC}$ and $\Delta_m\sin2\theta=a\sin2\theta_0$; in particular $\tan2\theta=a\sin2\theta_0/(a\cos2\theta_0-V_{CC})$ whenever the denominator is non-zero.
3. Matter eigenstates and eigenenergy difference (eqs. (92), (94)). For such $\theta$, $(\cos\theta,-\sin\theta)$ and $(\sin\theta,\cos\theta)$ are eigenvectors of $H$ with eigenvalues $(V_{CC}\mp\Delta_m)/2$, whose difference is $\Delta_m$.
4. Oscillation amplitude (eq. (97)). For such $\theta$ and $\Delta_m\neq0$, $\sin^2 2\theta$ equals the explicit resonance expression above.
5. MSW resonance (eq. (98)). The amplitude never exceeds $1$, and when $a\sin2\theta_0\ne0$ it equals $1$ exactly when $\sqrt2\,G_FN_e=\frac{\Delta m^2}{2E}\cos2\theta_0$.
6. Vacuum limit (text below eq. (96)). For $N_e=0$ and $\Delta m^2\ne0$: $\sin^22\theta=\sin^22\theta_0$ and $l_m=|l_{osc}|$.

Significance

Eq. (95) shows that at constant density the flavour transition has exactly the vacuum form with $\theta_0,l_{osc}$ replaced by $\theta,l_m$; together with the resonance condition (98) it underlies quantitative discussions of matter effects, from the solar neutrino problem to long-baseline experiments crossing the Earth. The milestones separate the linear-algebra content (diagonalizing a real symmetric $2\times2$ matrix) from the analytic content (solving a linear constant-coefficient ODE and the uniqueness of its solution).

The result is textbook material and is proved in the source. This mission adds a machine-checked derivation from the Schrödinger equation itself — including uniqueness of the solution of the initial-value problem, which the source leaves implicit — and reusable Lean definitions for later missions on the adiabatic (variable-density) regime of Section 8.3.

Difficulty

The algebra of eqs. (93)–(97) is elementary. The substantive step for a formal proof is the passage from "the Hamiltonian is diagonalized by a rotation" to "every solution of the ODE with the given initial datum has the stated $\nu_\mu$ component": this needs a uniqueness theorem for linear ODEs on $\mathbb C^2$ (or an equivalent argument). Degenerate parameter values ($\Delta_m=0$, $a\sin2\theta_0=0$) must be handled, since the Lean statements do not exclude them.

Formalization scope

All parameters are real numbers; the state is a function $\nu:\mathbb R\to\mathbb C^{2}$ (index $0=\nu_e$, $1=\nu_\mu$) assumed differentiable everywhere with derivative $-i\,H\nu(t)$, where $H$ is the real matrix above viewed as a complex matrix. The probability is the squared modulus $|\nu_\mu(L)|^2$. $E>0$ is assumed throughout; the sign of $\Delta m^2$, the value of $\theta_0$ and the density are unrestricted. Lean's division convention ($x/0=0$) applies to $l_m$ and $\sin^22\theta$ when $\Delta_m=0$; in that degenerate case $H$ is a multiple of the identity and both sides of the goal are $0$.

A statement that assumed the closed-form solution, or assumed the probability formula as a hypothesis, would be trivial; the goal instead quantifies over every solution of the initial-value problem. Proofs of any milestone, and reusable lemmas on uniqueness for linear constant-coefficient ODEs, are welcome.

Selected references

• E. Kh. Akhmedov, Neutrino physics, Trieste Summer School lectures, 1999. https://arxiv.org/abs/hep-ph/0001264
• L. Wolfenstein, Neutrino oscillations in matter, Phys. Rev. D 17 (1978) 2369. https://doi.org/10.1103/PhysRevD.17.2369
• S. P. Mikheyev, A. Yu. Smirnov, Resonance enhancement of oscillations in matter and solar neutrino spectroscopy, Sov. J. Nucl. Phys. 42 (1985) 913.

Motivation

Leptogenesis is a class of scenarios in which the baryon asymmetry of the Universe is produced from a lepton asymmetry generated in the out-of-equilibrium decays of heavy singlet neutrinos $N_k$, which also give the light neutrinos their small masses through the type I seesaw (Fukugita–Yanagida 1986). The review of Davidson, Nardi and Nir (Phys. Rep. 466 (2008) 105) collects the standard results of the field. One of its central quantitative facts is an upper bound on the CP asymmetry in the decays of the lightest singlet $N_1$, in terms of $M_1$ and the light-neutrino masses. This bound is the origin of the familiar lower bound $M_1\gtrsim10^9\,$GeV for thermal leptogenesis with hierarchical singlets (Eq. (5.12) of the review).

Timeline. Casas and Ibarra introduced the orthogonal-matrix parametrization of the seesaw in 2001 (hep-ph/0103065). Davidson and Ibarra derived the bound $|\varepsilon|\le 3M_1(m_3-m_1)/(16\pi v^2)$ on the total asymmetry in 2002 (hep-ph/0202239); Hamaguchi, Murayama and Yanagida gave a related bound (hep-ph/0109030). Once flavour effects were recognised (around 2006), attention moved to the flavoured asymmetries $\varepsilon_{\alpha\alpha}$, whose bound (Eq. (5.10) of the review) is the goal of this mission.

Setting

There are three lepton flavours $\alpha$ and three singlets $N_k$ with Majorana masses $M_k>0$. We work in the mass basis of the charged leptons and of the $N_k$. The Yukawa matrix $\lambda$ is an arbitrary complex $3\times3$ matrix, and $v=v_u>0$ is the Higgs vev. The light-neutrino mass matrix (Eq. (2.5)) is

$$[m]_{\alpha\beta}=\sum_k\lambda_{\alpha k}M_k^{-1}\lambda_{\beta k}v^2 ,$$

a complex symmetric matrix. It is diagonalized as $m=U^*D_mU^\dagger$ with $U$ unitary and $D_m=\operatorname{diag}(m_1,m_2,m_3)$, $m_i\ge0$ (Eq. (2.6)). The largest and smallest light masses are $m_{\max}$ and $m_{\min}$. The Casas–Ibarra matrix is $R=D_m^{-1/2}U^T\lambda D_M^{-1/2}v$ (Eq. (2.11)).

At tree level $N_1$ decays into $\phi\ell_\alpha$ and $\bar\phi\bar\ell_\alpha$ with partial rate $\Gamma_{\alpha\alpha}=|\lambda_{\alpha1}|^2M_1/(8\pi)$ and total rate $\Gamma_D=[\lambda^\dagger\lambda]_{11}M_1/(8\pi)$ (Eq. (4.5)). So the branching fractions satisfy $B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}=\Gamma_{\alpha\alpha}/\Gamma_D$. For hierarchical singlets the flavoured CP asymmetry is (Eq. (5.9))

$$\varepsilon_{\alpha\alpha}=\frac{3M_1}{16\pi v^2[\lambda^\dagger\lambda]_{11}}\operatorname{Im}\{[\lambda]_{\alpha1}[m^*\lambda]_{\alpha1}\}.$$

Formalization targets

Goal — Eq. (5.10)

$$|\varepsilon_{\alpha\alpha}|\le\frac{3M_1m_{\max}}{16\pi v^2}\sqrt{B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}}\qquad\text{for every flavour }\alpha.$$

Milestones

1. Eq. (2.6): the matrix $m$ admits a diagonalization $m=U^*D_mU^\dagger$ with $U$ unitary and $m_i\ge0$.
2. Eq. (2.11): for $m_i>0$, $R$ is complex orthogonal, $R^TR=RR^T=1$.
3. Sec. 5.2: $|m\cdot x^*|\le m_{\max}|x|$ for all $x\in\mathbb C^3$.
4. Sec. 5.2 / Eq. (5.17): the total asymmetry bound $|\sum_\alpha\varepsilon_{\alpha\alpha}|\le 3M_1(m_{\max}-m_{\min})/(16\pi v^2)$.

Significance

Eq. (5.10) is the input to the lower bounds on $M_1$ and on the reheat temperature for hierarchical thermal leptogenesis (Eq. (5.12), Sec. 9.4.3), and it shows that flavoured asymmetries are not suppressed for degenerate light neutrinos, unlike the total one (Eq. (5.17)). These are established results. The work here is to formalize them: to state the seesaw quantities precisely and machine-check the linear-algebra steps (Takagi factorization, complex orthogonality, operator-norm bounds) that the physics literature takes for granted. To the captain's knowledge none of these statements has a machine-checked proof.

Difficulty

The goal reduces to an operator-norm estimate for the complex symmetric matrix $m$. That estimate needs the diagonalization $m=U^*D_mU^\dagger$, which is a Takagi (Autonne–Takagi) factorization, not a unitary eigen-decomposition: $m$ is symmetric, not Hermitian. The obvious move, applying the spectral theorem to $m$, fails because $m$ is in general not normal. The milestone-1 existence statement therefore needs its own argument, for example through the Hermitian matrix $m^\dagger m$. The total-asymmetry bound (milestone 4) needs a finer argument than the triangle inequality to produce the difference $m_{\max}-m_{\min}$ rather than $m_{\max}$.

Formalization scope

• Everything is $3\times3$ over $\mathbb C$ with index set $\{0,1,2\}$ (Fin 3); the singlet "$N_1$" is index $0$.
• $m_{\max}$ and $m_{\min}$ are ⨆ i, masses i and ⨅ i, masses i over the three diagonal entries. No ordering of the $m_i$ is imposed.
• The diagonalization is a hypothesis IsLightMassDiagonalization m U masses (unitary $U$, $m_i\ge0$, $m=\overline U\,\mathrm{diag}(m_i)\,U^\dagger$). It is always satisfiable by milestone 1, so it is not vacuous.
• $\varepsilon_{\alpha\alpha}$ is the explicit hierarchical-limit expression (5.9), with $[\lambda^\dagger\lambda]_{11}$ written as $\sum_\beta|\lambda_{\beta1}|^2$. The physical approximation $M_{2,3}\gg M_1$ is built into this formula and is not a hypothesis. The branching sum is the tree-level ratio $\Gamma_{\alpha\alpha}/\Gamma_D$.
• Division by zero returns $0$ in Lean. This only matters when the first column of $\lambda$ vanishes, where both sides of the goal are $0$.
• Needed infrastructure: Takagi factorization of complex symmetric matrices (reusable beyond this mission), and elementary Euclidean-norm estimates on $\mathbb C^3$.

Selected references

• S. Davidson, E. Nardi, Y. Nir, Leptogenesis, Physics Reports 466 (2008) 105–177. https://doi.org/10.1016/j.physrep.2008.06.002 · https://arxiv.org/abs/0802.2962
• J. A. Casas, A. Ibarra, Oscillating neutrinos and μ → e γ, Nucl. Phys. B 618 (2001) 171. https://arxiv.org/abs/hep-ph/0103065
• S. Davidson, A. Ibarra, A lower bound on the right-handed neutrino mass from leptogenesis, Phys. Lett. B 535 (2002) 25. https://arxiv.org/abs/hep-ph/0202239
• M. Fukugita, T. Yanagida, Baryogenesis without grand unification, Phys. Lett. B 174 (1986) 45. https://doi.org/10.1016/0370-2693(86)91126-3

Motivation

In the note Reformulating String Theory with the 1/N Expansion (arXiv:hep-th/9405069), C. B. Thorn argues that stability and causality, which are manifest in quantum field theory but obscure in string theory, would become evident if strings were composite objects built from point-like constituents ("string bits"). The proposal combines the light-cone parametrization of the string with 't Hooft's $1/N$ expansion (G. 't Hooft, Nucl. Phys. B72 (1974) 461): bits are created by the entries of an $N\times N$ matrix field $\bar a(x)$, closed strings by the singlet traces $\mathrm{tr}\{\bar a(x_1)\cdots\bar a(x_M)\}$, and $1/N$ plays the role of the string coupling.

A load-bearing step of the proposal is that a long closed chain of $M$ bits behaves like a continuous string: in the continuum limit $M\to\infty$ with $P^+=M\epsilon T_0$ fixed, the finite-energy excitations must be string excitations. Thorn justifies this with the remark (p. 5) that "the low energy excitations of an $M$ particle discretized string are $O(1/M)\times$ the two-body level spacing". This mission formalizes that remark for the harmonic Hamiltonian written in the paper, together with the cyclic symmetry that ties the matrix traces to closed strings.

Setting

A discretized light-cone string with $M$ bits is described by transverse positions $x_1,\dots,x_M$ with cyclic identification $x_{M+1}=x_1$ and Hamiltonian (p. 4)

$$P^- = \frac1\epsilon\sum_{i=1}^{M}\frac{1}{2T_0}\Bigl(-\nabla_i^2 + T_0^2\,(x_{i+1}-x_i)^2\Bigr).$$

The potential term is the quadratic form of the cyclic Laplacian $L_M$, $(L_Mx)_i=2x_i-x_{i+1}-x_{i-1}$ (indices mod $M$), and the equations of motion are $\ddot x=-\epsilon^{-2}L_Mx$. A normal-mode frequency is an $\omega>0$ with $\epsilon^2\omega^2$ an eigenvalue of $L_M$; write $\Omega_{M,\epsilon}$ for the set of them. With $\hbar=1$ these are the excitation-level spacings of the chain.

The singlet creation operators are $\bar A(x_1,\dots,x_M)=(1/N)^{M/2}\mathrm{tr}\{\bar a(x_1)\cdots\bar a(x_M)\}$; since the $\bar a_{k\ell}$ commute with each other, cyclic invariance of the trace gives the cyclic symmetry $\psi_M(x_1,\dots,x_M)=\psi_M(x_2,\dots,x_M,x_1)$ of the string wave function.

Formalization targets

Goal

For all $M\ge2$ and $\epsilon>0$,

$$\min\Omega_{M,\epsilon}=\frac2\epsilon\sin\frac\pi M,\qquad \min\Omega_{2,\epsilon}=\frac2\epsilon,\qquad \min\Omega_{M,\epsilon}\le\frac\pi M\,\min\Omega_{2,\epsilon}.$$

Milestones

1. Cyclic symmetry: $\mathrm{tr}(a_0a_1\cdots a_M)=\mathrm{tr}(a_1\cdots a_Ma_0)$ for matrices over a commutative ring.
2. The bond potential is a quadratic form: $\sum_i(x_{i+1}-x_i)^2=x^{\mathsf T}L_Mx$.
3. Each $4\sin^2(\pi k/M)$ is an eigenvalue of $L_M$ ($M\ge1$).
4. Every eigenvalue of $L_M$ is $4\sin^2(\pi k/M)$ for some $0\le k<M$.

Significance

The goal is the quantitative content of the paper's continuum-limit argument in the harmonic case: the gap of an $M$-bit chain closes like $1/M$ relative to the two-body scale, so at fixed $P^+$ the low-lying spectrum approaches the equally spaced string spectrum. The same spectral facts about the cyclic Laplacian (the spectrum of the cycle graph) are used in lattice field theory and spectral graph theory, so the milestones are reusable outside this mission. The results are classical; the work here is their machine-checked formalization in a form tied to the string-bit Hamiltonian.

Difficulty

The trace and quadratic-form statements are finite algebra. The substance lies in the spectrum: exhibiting real eigenvectors for every $k$ needs trigonometric sum identities, and the completeness statement needs an argument that no other eigenvalues exist, which must handle the degenerate pairs $k\leftrightarrow M-k$. Identifying the least positive value then requires the symmetry $\sin(\pi k/M)=\sin(\pi(M-k)/M)$ and monotonicity of $\sin$ on $[0,\pi/2]$.

Formalization scope

• $L_M$ is a real matrix indexed by $\mathrm{Fin}\,M$; eigenvalues are those of the real linear map $x\mapsto L_Mx$ (nonzero real eigenvector).
• One transverse dimension is used; with $d-2$ transverse dimensions the modes decouple and the frequency set is the same. The tension $T_0$ drops out of the frequencies.
• "Two-body level spacing" is formalized as the lowest frequency of the $M=2$ member of the same cyclic family. The paper's claim for a general attractive potential $V$ (and the quantum field theory, the $1/N$ expansion itself, and the postscript remarks) is outside the scope.
• Edge cases: the goal assumes $M\ge2$ and $\epsilon>0$, so $\Omega_{M,\epsilon}$ is nonempty and its minimum is attained; the definition of $\Omega$ requires $\omega>0$, which excludes the zero mode.

Selected references

• C. B. Thorn, Reformulating String Theory with the 1/N Expansion, invited talk, First Int. A. D. Sakharov Conference (1991); arXiv:hep-th/9405069 (1994). https://arxiv.org/abs/hep-th/9405069
• G. 't Hooft, A planar diagram theory for strong interactions, Nucl. Phys. B72 (1974) 461.

Motivation

String/M theory appears to admit a very large number of four-dimensional vacua, and M. R. Douglas's 2003 paper The statistics of string/M theory vacua proposes to study them statistically: instead of constructing vacua one at a time, one places a measure on a space of effective theories and computes expected numbers and distributions of vacua. Two concrete mathematical ingredients of that programme are the subject of this mission.

The first is the Bousso–Polchinski counting of flux vacua (Section 3.6 of the paper, following Bousso–Polchinski 2000). Quantized fluxes form an integer vector $N\in\mathbb Z^J$, and the flux energy is a positive quadratic form in $N$. The number of flux choices with energy below $V$ controls whether a small cosmological constant can be realised; the paper evaluates the number distribution (3.13) by replacing the lattice sum with an integral, obtaining a density proportional to $V^{J/2-1}\,dV$.

The second is the Gaussian ensemble of superpotentials (Section 4 and 4.1): a random polynomial superpotential whose coefficients are independent complex Gaussians, with an explicit normalising constant and an explicit count of coefficients.

Setting

Fix an integer $J\ge 0$ (the number of independent flux quanta, $J=b_{p+1}$ in the paper) and a constant $c>0$ (in the paper $c=M_{pl}^2/(M^{2p}V_{p+1}^2)$). For a flux vector $N=(N_1,\dots,N_J)\in\mathbb Z^J$ the flux potential is

$$V(N)=c\sum_{i=1}^J N_i^2 ,$$

and the flux vacua count below level $V$ is

$$\mathcal N_J(c,V)=\#\{N\in\mathbb Z^J : V(N)\le V\}.$$

This is the cumulative distribution function of the measure $d\mu(V)=\sum_N\delta(V-V(N))$ of eq. (3.13). The unit ball in $\mathbb R^J$ has volume $\omega_J=\pi^{J/2}/\Gamma(J/2+1)$, and the unit sphere has area $\mathrm{Vol}(S^{J-1})=2\pi^{J/2}/\Gamma(J/2)=J\omega_J$.

For the superpotential ensemble, a polynomial in $n$ variables of degree at most $d$ has one coefficient per monomial $z^{I}=z_1^{I_1}\cdots z_n^{I_n}$ with $|I|\le d$; the paper states there are $c(d,n)=(d+n)!/(d!\,n!)$ of them. The coefficients $w_I\in\mathbb C$ are given the weight $(\alpha/\pi)^{c(d,n)}\prod_I d^2w_I\,e^{-\alpha|w_I|^2}$, $\alpha>0$, which the paper says is unit normalised.

Formalization targets

Goal: asymptotic count of flux vacua

$$\lim_{V\to\infty}\frac{\mathcal N_J(c,V)}{(V/c)^{J/2}}=\frac{\pi^{J/2}}{\Gamma(J/2+1)} .$$

This is the precise, integrated form of the approximation in (3.13): integrating $\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}v^{J/2-1}$ from $0$ to $V$ gives exactly $\omega_J (V/c)^{J/2}$.

Milestones

1. Finiteness: for every $V$, only finitely many $N\in\mathbb Z^J$ satisfy $V(N)\le V$ (so $\mathcal N_J$ is a genuine count).
2. Continuum volume: the Lebesgue volume of $\{x\in\mathbb R^J : c\sum x_i^2\le V\}$ equals $\omega_J (V/c)^{J/2}$ for $V\ge 0$.
3. Continuum density (3.13): for $0\le V_1\le V_2$ and $J\ge1$, the volume of the shell $\{V_1<c\sum x_i^2\le V_2\}$ equals $\int_{V_1}^{V_2}\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}\,v^{J/2-1}\,dv$.
4. Coefficient count: $\#\{I\in\mathbb N^n : |I|\le d\}=\#\{I\in\mathbb N^{n+1} : |I|=d\}=(d+n)!/(d!\,n!)$.
5. Normalisation of the complex Gaussian ensemble: $\int_{\mathbb C^m}(\alpha/\pi)^m e^{-\alpha\sum_I|w_I|^2}\,d^{2m}w=1$ for every $m$ and $\alpha>0$.

Significance

The goal makes rigorous the step "replace the sum with an integral" that underlies the Bousso–Polchinski estimate of how many flux vacua lie below a given energy, with the exact constant appearing in (3.13). Milestones 4 and 5 certify the combinatorial and analytic constants of the Gaussian ensemble (4.6) on which the paper's densities (4.7)–(4.10) are built. None of these results is new mathematics: the goal is the $J$-dimensional analogue of the Gauss circle problem at leading order, and the milestones are classical. What the mission adds is a machine-checked version of the precise constants used in the paper.

Difficulty

The goal requires comparing a lattice-point count with a volume. The naive bound, counting unit cubes centred at lattice points, must be controlled uniformly: cubes meeting the boundary of the ball contribute an error of order $R^{J-1}$ with $R=\sqrt{V/c}$, and one has to show that this is $o(R^J)$. The volume formula for Euclidean balls expressed through the Gamma function, and its transport to the product space $\mathbb R^J$ with the sum-of-squares form, is further required infrastructure.

Formalization scope

• Flux vectors are functions Fin J → ℤ; the count uses Set.ncard, whose value on an infinite set would be $0$ — milestone 1 rules out that degenerate reading.
• Continuum statements use the product Lebesgue measure on Fin J → ℝ (not EuclideanSpace), with the quadratic form $c\sum x_i^2$ written out explicitly.
• The Gaussian ensemble is formalised only for complex coefficients (the "GUE" case). For real coefficients the paper's constant $(\alpha/\pi)^{c(d,n)}$ would not normalise the measure (the correct constant is $(\alpha/\pi)^{c(d,n)/2}$), so the real case is deliberately omitted.
• The paper's finiteness conjecture (3.16) for full string compactifications, and the densities (4.7)–(4.10), are not formalised; they are not stated precisely enough in the source.
• Definitions: DouglasVacua.fluxPotential, DouglasVacua.fluxVacuaCount.

Selected references

• M. R. Douglas, The statistics of string/M theory vacua, JHEP 05 (2003) 046. https://doi.org/10.1088/1126-6708/2003/05/046 — arXiv:hep-th/0303194
• R. Bousso, J. Polchinski, Quantization of four-form fluxes and dynamical neutralization of the cosmological constant, JHEP 06 (2000) 006. https://arxiv.org/abs/hep-th/0004134

Motivation

Gambini and Pullin (IJMPD 23 (2014) 1442023) study quantum fields living on the discrete quantum spacetimes of spherically symmetric loop quantum gravity. Discreteness makes the field equations lattice-like and hence breaks Lorentz invariance. Collins, Perez, Sudarsky, Urrutia and Vucetich (PRL 93 (2004) 191301) argued that in interacting theories such Planck-scale violations feed, through renormalized loop diagrams, into large low-energy violations: a difference of second derivatives of the self-energy that should vanish by Lorentz invariance stays bounded away from zero. Gambini and Pullin argue that two exponential weights — a Gaussian fuzziness factor from the spread of the ADM mass, and a Lorentz-invariant nonlocal interaction factor of the type found in string field theory — make this quantity arbitrarily small.

Because the full self-energy calculation is lengthy, the paper's Appendix A replaces it by a two-dimensional model integral in which rotations play the role of Lorentz transformations and a parameter $\sigma$ plays the role of lattice spacing. This mission formalizes the precise mathematical claims made about that model.

Setting

For real parameters $\sigma \ge 0$ define the denominator base and the model integrand

$$D_\sigma(x,y) = 1 + x^2 + \frac{y^2}{1+\sigma y^2}, \qquad f_\sigma(x,y) = \frac{x^2-y^2}{D_\sigma(x,y)^2}.$$

The paper's integral (A.1) is $I = \int_{\mathbb R^2} f_\sigma(x,y)\,dx\,dy$. For $\sigma = 0$ one has $D_0 = 1 + x^2 + y^2$, which is rotation invariant.

(A.1) is only a formal expression: $f_\sigma$ is not Lebesgue integrable on $\mathbb R^2$ (for $\sigma = 0$ it decays like $r^{-2}$; for $\sigma > 0$ it grows like $-y^2$ along the $y$-axis). The mission therefore uses the disk-truncated integral

$$I^{\mathrm{disk}}_\sigma(R) = \int_{x^2+y^2 \le R^2} f_\sigma(x,y)\,dx\,dy,$$

which regularizes (A.1) in a rotation-invariant way.

The weighted model integral (A.2) is, for weights $\alpha, \beta$,

$$I(\alpha,\beta,\sigma) = \int_{\mathbb R^2} e^{-\alpha x^2}\, e^{-\beta(x^2+y^2)}\, f_\sigma(x,y)\,dx\,dy .$$

The first factor models the fuzziness (it acts on one direction only), and the second models the nonlocal interaction (rotation invariant here, Lorentz invariant in the physical case).

Formalization targets

Goal (Appendix A, sentence after (A.2))

"With suitable choices of $\alpha$ and $\beta$ one can make the integral as small as desired":

$$\forall \sigma > 0,\ \forall \varepsilon > 0,\ \exists \alpha > 0,\ \exists \beta > 0:\quad |I(\alpha,\beta,\sigma)| < \varepsilon .$$

Milestones

1. For $\sigma = 0$ the integral vanishes: $I^{\mathrm{disk}}_0(R) = 0$ for every $R$.
2. For $\sigma > 0$ it "does not vanish by a significant amount": $I^{\mathrm{disk}}_\sigma(R) \to -\infty$ as $R \to \infty$.
3. (A.2) is well defined: the weighted integrand is integrable for $\alpha \ge 0$, $\beta > 0$, $\sigma \ge 0$.
4. With only the rotation-invariant weight and $\sigma = 0$, (A.2) still vanishes: $I(0,\beta,0) = 0$ for $\beta > 0$.
5. In the regime $\alpha \sim \beta$ large: $I(\beta,\beta,\sigma) \to 0$ as $\beta \to \infty$, for each $\sigma > 0$.

Significance

In the paper this model is the only precisely stated mathematical content backing the claim that the two exponential weights restore approximate Lorentz invariance. Formalizing it pins down exactly which statements hold (and in what sense the formal integral (A.1) "vanishes" or "does not vanish"), separating the rigorous content of the toy model from the physical argument it illustrates. The results are elementary real analysis; no machine-checked proofs of them are known to exist.

Difficulty

The main difficulty is that the unweighted integral (A.1) diverges, so both "vanishes" and "does not vanish" need a regularization. The weighted statements need integrability and dominated-convergence estimates on $\mathbb R^2$ and a change of variables (swapping $x$ and $y$) for the symmetry claims. The divergence to $-\infty$ in milestone 2 needs separate upper and lower estimates for the positive and negative parts of $f_\sigma$ on growing disks.

Formalization scope

All objects are real-valued functions on $\mathbb R \times \mathbb R$ with Lebesgue (product) measure. $I(\alpha,\beta,\sigma)$ is a Bochner integral over the whole plane; where the integrand is not integrable, the Lean integral is $0$ by convention, which is why milestone 3 is included and all weighted statements assume $\beta > 0$. The disk is the closed Euclidean disk $\{x^2+y^2 \le R^2\}$, not a sup-norm ball. The parameter $\sigma$ is restricted to $\sigma \ge 0$ (or $\sigma > 0$) wherever it matters, so that $1+\sigma y^2 > 0$. The sentence in the paper "more precisely one needs $\alpha \sim \beta$ and both larger than $\sigma$" is heuristic; only its sufficiency direction along $\alpha = \beta$ is formalized (milestone 5). No necessity claim is formalized, because a large $\beta$ alone already makes $I$ small.

Selected references

• R. Gambini, J. Pullin, Emergence of stringlike physics from Lorentz invariance in loop quantum gravity, Int. J. Mod. Phys. D 23 (2014) 1442023. https://doi.org/10.1142/S0218271814420231
• J. Collins, A. Perez, D. Sudarsky, L. Urrutia, H. Vucetich, Lorentz invariance and quantum gravity: an additional fine-tuning problem?, Phys. Rev. Lett. 93 (2004) 191301. https://doi.org/10.1103/PhysRevLett.93.191301

Motivation

A hierarchy of infinitely many overlap scales need not fill an interval. Full support asks whether an admissible zero-temperature SK minimizer leaves any gap below overlap one. The pinned manuscript supplies the research context.

Setting

An order parameter is a nonnegative, monotone, right-continuous integrable function on [0,1). The Parisi value is defined by a Brownian stochastic-control supremum. The Stieltjes measure μ lives on the subtype Time=[0,1); its support below is taken in that relative topology.

Formalization target

The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is

$$\operatorname{supp}\mu=[0,1),\qquad \mathbb E[u_x(t,X_t)^2]=t,\quad\mathbb E[u_{xx}(t,X_t)^2]=1.$$

The theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.

Significance and status

The main target is the five-part full-support conclusion for every encoded minimizer and Brownian system. The separate value-consequences bundle is retained as an additional formal target. 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 conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.

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.SKValue.value_consequences (Open).

Selected references

• OpenAI, Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Random site energies change the spectral behavior of a lattice Schrödinger operator. Identifying its almost-sure spectrum is one part of the planar Anderson problem. The pinned manuscript supplies the research context.

Setting

The lattice is the integer plane. A state is a square-summable complex function on its sites, and the potential at each site is independently uniform on the interval from −h to h, with h positive.

Formalization target

The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is

$$\sigma(H_v)=[-4-h,4+h].$$

The theorem states that for every real h>0, for almost every disorder configuration v under disorderLaw(h), there exists a bounded complex-linear operator H on the Hilbert space ℓ²(ℤ², ℂ) of square-summable complex functions on the planar lattice ℤ×ℤ such that H is an Anderson operator for v, H is self-adjoint, and the spectrum of H in ℂ equals the real interval [-4-h, 4+h] (embedded in ℂ as the points with imaginary part 0). Here a configuration is a real-valued function v on lattice sites, and disorderLaw(h) is the infinite product measure over sites of the uniform distribution (Lebesgue measure conditioned on the interval) on [-h,h], so the potential values are independent. H is an Anderson operator for v when, for every u in ℓ² and every site x=(a,b), (Hu)(a,b) = u(a+1,b)+u(a-1,b)+u(a,b+1)+u(a,b-1)+v(a,b)u(a,b), the sum of the four nearest-neighbour values plus the local potential times u at x. The statement is recorded as an admitted theorem.

Significance and status

The selected goal asserts existence, self-adjointness and the spectrum interval. Pure-point spectral type, a complete eigenbasis and dynamical localization are not conclusions of this published target. 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 interval must be identified almost surely for an infinite random operator, including both exclusion of spectrum outside the interval and inclusion of its interior.

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, Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.

Setting

A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on $J$, while the same spins are pinned on $F$ and a target event is prescribed on $I$.

Formalization targets

$$e^{-4\operatorname{artanh}q_0}\le\frac{\mu_{\mathrm{mix}}(\sigma_I=a\mid\sigma_F=\tau)}{\mu_{\mathrm{mix}'}(\\sigma_I=a\\mid\\sigma_F=\\tau)}\\le e^{4\\operatorname{artanh}q_0}.$$

A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).

The goal is OAI.BufferedIsing.finite_graph_comparison.

Significance

The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. 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

Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.

Formalization scope

The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets $I,J,F$ are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.

The shared definitions are supplied by BufferedIsing. 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, Buffered comparison and stopping-band resolution in critical Ising, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation: continuum phase transitions with a power-law tail

Whether identical classical particles in $\mathbb R^3$, interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.

Timeline

• 1965 — Motzkin and Straus's weighted-graph maximization, later used for occupation bounds (Motzkin–Straus 1965).
• 1966 — Lebowitz and Penrose: rigorous van der Waals–Maxwell theory in the Kac limit (Lebowitz–Penrose 1966).
• 1970 — Ruelle's superstability framework (Ruelle 1970).
• 1971 — Ruelle: transition for a symmetric two-species continuum system (Ruelle 1971).
• 1973 — Gerardi, Marchioro, Olivieri and Presutti extend the Lebowitz–Penrose limit to superstable references (GMOP 1973).
• 1984 — Simon lists the problem among fifteen problems in mathematical physics.
• 1998–1999 — Lebowitz, Mazel and Presutti: liquid–vapor transition with attractive pair and repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
• 2026 — He, Jauslin, Lebowitz and Peled: transition for a finite-range box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: density coexistence for saturated many-body interactions (arXiv:2602.11078).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026): a radial potential with divergent core and $o(r^{-3})$ tail with a temperature singularity, and the present A radial continuum phase transition with algebraic decay, which claims a bounded continuous potential with $|\phi(r)|\le Cr^{-3-1/32}$. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Particles live in $\mathbb R^3$; a radial pair potential is a function $\phi:[0,\infty)\to\mathbb R$ (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube $\Lambda_L=[0,L]^3$ and $N\ge0$,

$$U^\phi(x_1,\dots,x_N)=\sum_{i<j}\phi(|x_i-x_j|),\qquad Z_{L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U^\phi}\,dx,\qquad Z_{L,0}=1 .$$

The potential is stable if $U^\phi\ge -BN$ for all configurations. The canonical free energy at density $\rho$ is

$$f(\beta,\rho)=-\lim_{L\to\infty}\frac1{\beta L^3}\log Z_{L,\lfloor\rho L^3\rfloor}(\beta).$$

The packing constant is $p=\lim_{L\to\infty}M_L/L^3$, where $M_L$ is the largest number of points in $[0,L]^3$ at mutual distance $\ge1$; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at $\beta_c$ with the right one strictly smaller, and non-differentiability.

Formalization targets

Milestone: the corner at the central density

At the single density $\rho=5p/3$: there are a bounded continuous stable $\phi$ with $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$ and $\beta_c\in[7/8,9/8]$ such that $f(\cdot,5p/3)$ exists for all $\beta>0$ and

$$f'_-(\beta_c,5p/3)>f'_+(\beta_c,5p/3).$$

Goal: a common corner on a density interval

There are a bounded continuous $\phi$, constants $B,C>0$ with

$$\sum_{i<j}\phi(|x_i-x_j|)\ge -BN,\qquad |\phi(r)|\le C\,r^{-3-1/32}\ (r\ge1),$$

an open interval $I=(5p/3-\eta,\,5p/3+\eta)\subset(0,\infty)$ and one $\beta_c\in[7/8,9/8]$ such that for every $\rho\in I$ the free energy $f(\beta,\rho)$ exists and is finite for every $\beta>0$, and

$$f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).$$

This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.

Significance

The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an $o(r^{-3})$ tail; the fixed power margin $1/32$ here needs a quantitative range estimate not present there.

Formalizing it. The statement fixes the model completely (free boundary conditions on $[0,L]^3$, Lebesgue measure without temperature normalization, $1/N!$, $\lfloor\rho L^3\rfloor$ particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.

Difficulty

The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.

Formalization scope

• Positions are EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with $B>0$, and decay with $C>0$ are separate conjuncts.
• $p$ is existentially quantified but pinned by IsPackingDensity p (a limit), and $p>0$ is required; packingNumber is a sSup over a bounded set of naturals.
• IsCanonicalFreeEnergy φ ρ f asserts $-\log Z/(\beta L^3)\to f(\beta)$ for every $\beta>0$, so $f$ is determined on $(0,\infty)$; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.
• The goal requires the interval to lie in $(0,\infty)$ and $\beta_c$ to be independent of $\rho$.
• Needed infrastructure: superstability and occupation moments, existence of thermodynamic limits and their convex duality, a Motzkin–Straus bound, quantitative Kac comparison, and subdifferential persistence arguments.

Selected references

• B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
• T. S. Motzkin and E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canad. J. Math. 17 (1965), 533–540. https://doi.org/10.4153/CJM-1965-053-6
• J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
• D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
• D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
• A. Gerardi, C. Marchioro, E. Olivieri and E. Presutti, Van der Waals–Maxwell theory, Lebowitz–Penrose limit and superstable interactions, Comm. Math. Phys. 29 (1973), 219–231. https://doi.org/10.1007/BF01645248
• J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
• Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid-vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
• D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf
• OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf