Mathematical Physics

Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.

Motivation

Dirac showed in 1931 that quantum mechanics permits isolated magnetic charges provided electric charge is quantized, but in Maxwell's theory such a magnetic monopole is a point singularity attached to an unobservable "Dirac string". In 1974 G. 't Hooft and, independently, A. M. Polyakov observed that in gauge theories where the electromagnetic group $U(1)$ sits inside a larger group with compact covering group, monopoles arise instead as smooth, finite-energy solutions of the classical field equations, with no singularity and no string. 't Hooft's paper (Nucl. Phys. B79 (1974) 276) does this for the SO(3) model of Georgi and Glashow and computes the mass numerically. The resulting "'t Hooft–Polyakov monopole" became the model example of a topological soliton in gauge theory.

Timeline. 1931: Dirac's quantization argument (Proc. R. Soc. A 133, 60). 1972: Georgi–Glashow SO(3) electroweak model (PRL 28, 1494). 1974: 't Hooft and Polyakov (JETP Lett. 20, 194) describe the regular monopole, 't Hooft by a spherically symmetric ansatz, a reduced one-dimensional energy functional and a numerical minimisation. 1975: Prasad and Sommerfield find a closed-form solution in the limit $\lambda \to 0$ (PRL 35, 760). For $\lambda > 0$ no closed form is known.

Setting

Space and isospin space are both $\mathbb R^3$. A static configuration in the gauge $W_4 = 0$ consists of a Higgs triplet $Q_a(x)$ and a gauge field $W^a_i(x)$, $i, a \in \{1,2,3\}$. With coupling $e$, Higgs self-coupling $\lambda$ and vacuum value $F$ (eqs. (2.1)–(2.3), with $\mu^2 = -\tfrac12\lambda F^2$),

$$D_iQ_a = \partial_iQ_a + e\,\varepsilon_{abc}W^b_iQ_c,\qquad G^a_{ij} = \partial_iW^a_j - \partial_jW^a_i + e\,\varepsilon_{abc}W^b_iW^c_j,$$

and the static energy is

$$E[Q,W] = \int_{\mathbb R^3}\Big(\tfrac14 G^a_{ij}G^a_{ij} + \tfrac12 D_iQ_a\,D_iQ_a + \tfrac18\lambda\,(Q_aQ_a - F^2)^2\Big)\,d^3x .$$

The vector masses are $M_W = eF$ and the Higgs mass is $M_H = \sqrt\lambda F$. A static solution is a smooth configuration of finite energy at which $E$ is stationary under all compactly supported smooth variations. 't Hooft's gauge-invariant electromagnetic tensor (2.17) is

$$F_{ij} = \frac{1}{|Q|}Q_aG^a_{ij} - \frac{1}{e|Q|^3}\varepsilon_{abc}Q_a(D_iQ_b)(D_jQ_c).$$

The spherically symmetric ansatz (2.8) is $Q_a(x) = x_aQ(r)$, $W^a_i(x) = \varepsilon_{iab}x_bW(r)$ with $r = |x|$. The monopole boundary condition is $Q_a(x) \to F x_a/r$ as $r \to \infty$ (eqs. (2.6), (2.11)).

Formalization targets

Goal (Sect. 2 and abstract)

For all $e > 0$, $\lambda > 0$, $F > 0$ there are radial profiles $Q(r), W(r)$ such that the configuration (2.8) is a smooth finite-energy static solution with

$$Q_a(x) - F\frac{x_a}{|x|} \to 0,\qquad |x|^2F_{ij}(x) + \frac1e\,\varepsilon_{ija}\frac{x_a}{|x|} \to 0\qquad(|x|\to\infty),$$

i.e. a regular magnetic monopole whose far field is (2.20).

Milestones

1. Eq. (1.5): $\Omega\Omega^\dagger = 1$ for the SU(2) matrix (1.4).
2. Eq. (2.6): the adjoint action of $\Omega$ sends the isovector $(0,0,1)$ to a unit radial isovector.
3. Sect. 2: the boundary condition forces the Higgs field to vanish somewhere.
4. Eq. (2.9): reduced energy density of the ansatz.
5. Eq. (2.13): the Lagrange equation for $W$.
6. Eqs. (2.14)–(2.15): the only power law $W = ar^{-n}$ compatible with (2.13) and $Q = F/r$ is $n = 2$, $a = -1/e$.
7. Eqs. (2.18)–(2.20): the asymptotic fields have $D_iQ_a = 0$ and $F_{ij} = -\varepsilon_{ija}x_a/(er^3)$.
8. Eq. (2.21): total magnetic flux of magnitude $4\pi/e$.
9. Eq. (3.2): the energy in the dimensionless variables $x = eFr$, $\beta = \lambda/e^2$.

Significance

The existence of a regular monopole is what makes the monopole a particle of the theory: its mass $M_m = \frac{4\pi}{e^2}M_WC(\beta)$ (eq. (3.3)) is finite and calculable, and its magnetic charge is fixed by topology rather than put in by hand. The ingredients (hedgehog ansatz, the zero of the Higgs field forced by the boundary condition, the reduction to an ODE system, the gauge-invariant electromagnetic tensor) are reused throughout the theory of solitons in gauge theories.

The result is established in the physics literature; 't Hooft's own argument is partly numerical (trial functions). The mission asks for a machine-checked development: the algebraic and calculus identities of Sects. 1–3, the topological zero, and a complete existence proof for the spherically symmetric solution for every $\lambda > 0$. No machine-checked proof of any of these is known to the proposer.

Difficulty

The identities (milestones 1, 4, 6–9) are finite computations, but milestones 4, 5 and 9 must go through Fréchet derivatives of vector fields on $\mathbb R^3$ and spherical coordinates, where most of the work lies. Milestone 3 is a degree-theoretic statement not available off the shelf. The goal needs an actual existence theorem for a nonlinear coupled ODE system on $(0,\infty)$ with singular coefficients at $r = 0$ and boundary conditions at both ends, followed by regularity of the resulting fields at the origin and the passage from the reduced (radial) equations to the full field equations. 't Hooft's numerical minimisation over trial functions gives no proof that a minimiser exists or is smooth.

Formalization scope

$\mathbb R^3$ is EuclideanSpace ℝ (Fin 3) with Lebesgue measure; indices run over Fin 3 = {0,1,2}, the Levi-Civita symbol is an explicit formula, partial derivatives are Fréchet derivatives in coordinate directions. Fields are static and in the gauge $W_4 = 0$, where the Gauss-law equation holds automatically, so "static solution" means: $C^\infty$ fields, integrable energy density, and zero derivative of the energy along every smooth compactly supported variation of $Q$ and $W_i$. Lean's total operations are used: division by zero is $0$ and the Bochner integral of a non-integrable function is $0$; every statement using them either excludes the degenerate input or is insensitive to it (the goal demands integrability explicitly). The constant $\tfrac18\lambda F^4$ is included so the vacuum has zero energy, as in (2.9).

Two deviations from the printed text, both flagged in the milestones: (i) with standard Pauli matrices, $\Omega\sigma_3\Omega^\dagger$ is $(\sin\theta\sin\varphi,\ \sin\theta\cos\varphi,\ \cos\theta)\cdot\vec\sigma$, whereas (2.6) prints $(\sin\theta\cos\varphi,\ \sin\theta\sin\varphi,\ \cos\theta)$; the milestone states the computed identity. (ii) With $B_k = \tfrac12\varepsilon_{kij}F_{ij}$, (2.20) gives $B = -x/(er^3)$ while (2.21) prints $+x/(er^3)$; the flux milestone therefore states the magnitude $4\pi/e$, and the sign is fixed by (2.20). The asymptotic analysis (2.14)–(2.15) is formalized as an exact statement about pure power laws. The numerical values of $C(\beta)$ in (3.3) are not formalized.

A trivializing reading of the goal is ruled out: the solution must satisfy the non-trivial boundary condition, which by milestone 3 excludes the vacuum, and the stationarity must hold for all variations, not only spherically symmetric ones.

Useful reusable infrastructure: spherical-coordinate integration of radial functions on $\mathbb R^3$, calculus of hedgehog fields, and a Brouwer-degree / no-retraction argument for maps of the sphere. Contributions of any milestone, and of alternative existence proofs (variational, shooting), are welcome.

Selected references

• G. 't Hooft, Magnetic monopoles in unified gauge theories, Nucl. Phys. B79 (1974) 276–284. https://doi.org/10.1016/0550-3213(74)90486-6
• A. M. Polyakov, Particle spectrum in quantum field theory, JETP Lett. 20 (1974) 194.
• P. A. M. Dirac, Quantised singularities in the electromagnetic field, Proc. R. Soc. A 133 (1931) 60. https://doi.org/10.1098/rspa.1931.0130
• H. Georgi, S. L. Glashow, Unified weak and electromagnetic interactions without neutral currents, Phys. Rev. Lett. 28 (1972) 1494. https://doi.org/10.1103/PhysRevLett.28.1494
• M. K. Prasad, C. M. Sommerfield, Exact classical solution for the 't Hooft monopole and the Julia–Zee dyon, Phys. Rev. Lett. 35 (1975) 760. https://doi.org/10.1103/PhysRevLett.35.760

Motivation

General relativity predicts that a black hole, once it has settled down after collapse, retains almost no memory of the matter that formed it. The no-hair theorem, also called the black hole uniqueness theorem, states that all stationary black-hole solutions of the Einstein–Maxwell equations are completely characterized by three externally observable parameters: mass, angular momentum and electric charge; all other information ("hair") disappears behind the event horizon. The phrase "black holes have no hair" was popularized by John Archibald Wheeler. Its observational content is tested in gravitational-wave ringdown signals and in black-hole imaging.

Despite its name, there is no rigorous proof of the general statement: mathematicians refer to it as the no-hair conjecture.

Timeline.

• 1967 — W. Israel proves uniqueness of the Schwarzschild metric among static vacuum black holes (Phys. Rev. 164, 1776).
• 1968 — Israel extends this to static electrovacuum black holes, obtaining Reissner–Nordström (Commun. Math. Phys. 8, 245).
• 1971 — B. Carter shows that an axisymmetric vacuum black hole has only two degrees of freedom (Phys. Rev. Lett. 26, 331); D. C. Robinson later completes uniqueness of Kerr.
• 1970s — S. Hawking's rigidity theorem, combined with Carter and Robinson, yields uniqueness of Kerr in vacuum under the additional hypotheses of non-degenerate horizons and real analyticity of spacetime.
• 2007 — extension to positive cosmological constant (Bhattacharya–Lahiri, arXiv:gr-qc/0702006).

Counterexamples are known in dimensions above four, for non-abelian Yang–Mills fields and for some non-minimally coupled scalar fields; this mission concerns only the four-dimensional Einstein–Maxwell theory with zero cosmological constant.

Setting

A spacetime is a smooth 4-manifold $M$ with a Lorentzian metric $g$ of signature $(-,+,+,+)$, an electromagnetic field $F$ (a 2-form) and a time orientation $T$. The pair $(g,F)$ is electrovacuum if, in geometrized Gaussian units,

$$G_{\mu\nu}=2\Big(F_{\mu\alpha}F_\nu{}^\alpha-\tfrac14g_{\mu\nu}F_{\alpha\beta}F^{\alpha\beta}\Big),\qquad\nabla_\mu F^{\mu\nu}=0,\qquad dF=0 .$$

The spacetime is stationary if a one-parameter group $\varphi_t$ of isometries preserves $F$, and it has a stationary asymptotically flat end $M_{\rm ext}$ if coordinates $(t,\vec x)$, $|\vec x|>R$, cover an open set on which $\varphi_t$ is the time translation and $g_{\mu\nu}-\eta_{\mu\nu}=O(1/|\vec x|)$, $\partial g=O(1/|\vec x|^2)$, $F=O(1/|\vec x|^2)$.

With $I^\pm$ the chronological future and past, the domain of outer communications is $\langle\langle M_{\rm ext}\rangle\rangle=I^+(M_{\rm ext})\cap I^-(M_{\rm ext})$, the black-hole region is $M\setminus I^-(M_{\rm ext})$ and the future event horizon is $\partial I^-(M_{\rm ext})$.

The Kerr–Newman family, in Kerr–Schild coordinates, is $g^{KN}=\eta+f\,k\otimes k$ with

$$f=\frac{r^2(2mr-e^2)}{r^4+a^2z^2},\qquad k=\Big(1,\frac{rx+ay}{r^2+a^2},\frac{ry-ax}{r^2+a^2},\frac zr\Big),\qquad \frac{x^2+y^2}{r^2+a^2}+\frac{z^2}{r^2}=1,$$

with potential $A=\frac{er^3}{r^4+a^2z^2}k$. For $m>0$, $a^2+e^2\le m^2$ its domain of outer communications is $\{r>r_+\}$, $r_+=m+\sqrt{m^2-a^2-e^2}$.

Formalization targets

Goal: the no-hair conjecture

Under the standing hypotheses (smooth electrovacuum, stationary, asymptotically flat end, globally hyperbolic $\langle\langle M_{\rm ext}\rangle\rangle$, nonempty black-hole region, connected event horizon), there are $m>0$, $a$, $e$ with $a^2+e^2\le m^2$, an angle $\beta$ and a diffeomorphism $\Psi$ with

$$\Psi:\{r>r_+\}\xrightarrow{\cong}\langle\langle M_{\rm ext}\rangle\rangle,\qquad\Psi^*g=g^{KN}_{m,a,e},\qquad\Psi^*F=\cos\beta\,F^{KN}+\sin\beta\,\star F^{KN}.$$

Milestones

1. The Kerr–Newman metric solves the Einstein–Maxwell equations where $r>0$.
2. Kerr–Newman black holes satisfy the standing hypotheses (the goal is not vacuous).
3. Israel 1967: static vacuum $\Rightarrow$ Schwarzschild ($a=e=0$).
4. Israel 1968: static electrovacuum $\Rightarrow$ Reissner–Nordström ($a=0$).
5. Carter 1971 / Robinson: axisymmetric vacuum $\Rightarrow$ Kerr ($e=0$).
6. Hawking–Carter–Robinson: analytic vacuum with non-degenerate horizon $\Rightarrow$ Kerr.
7. Frame normalization: a Lorentz boost takes a timelike 4-momentum to rest, $\Lambda P=(\sqrt{-P^2},0,0,0)$.
8. Frame normalization: a rotation aligns the spin, $RJ=(0,0,|J|)$.

Significance

A proof of the goal would establish that the Kerr–Newman metrics exhaust the stationary, asymptotically flat electrovacuum black holes with connected horizon, which is the mathematical basis for treating astrophysical black holes as described by three numbers. It would also remove the analyticity and non-degeneracy hypotheses from the known vacuum results.

No machine-checked proof of any statement in this mission is known. Milestones 1, 7 and 8 are classical computations; milestones 3–6 are published theorems whose proofs rely on substantial Lorentzian geometry and elliptic PDE; the goal is open.

Difficulty

Uniqueness proofs reduce the problem to an elliptic boundary-value problem on the orbit space once enough symmetry is available. In the general stationary case the extra axial symmetry is not known to exist: Hawking's rigidity argument produces it only for analytic metrics, because it extends a Killing field off the horizon by analytic continuation. Without analyticity, unique continuation for the Killing equation across the horizon is the obstruction. Degenerate (extremal) horizons further break arguments that rely on a bifurcation surface.

Formalization scope

Spacetimes are Mathlib smooth manifolds modelled on EuclideanSpace ℝ (Fin 4); the metric and field are fields of continuous bilinear forms on tangent spaces, and curvature and field equations are imposed through components in every chart. Causal sets use $C^1$ curves parametrized by $[0,1]$. The Kerr–Newman comparison spacetime is the region $\{r>r_+\}$ of Kerr–Schild coordinate space with the explicit metric. Magnetic charge is accommodated by the duality angle $\beta$.

The hypotheses are not vacuous: milestone 2 asserts that every Kerr–Newman black hole satisfies them. The connected-horizon hypothesis excludes the static multi-black-hole Majumdar–Papapetrou solutions, which would otherwise contradict the goal.

Needed infrastructure: Levi-Civita connection and curvature on manifolds, causal theory (global hyperbolicity, Cauchy surfaces), Killing fields and their flows, and the elliptic theory of harmonic maps used in uniqueness proofs. Contributions on any of these, and on milestones 1, 7 and 8, are welcome.

Selected references

• Wikipedia, No-hair theorem, revision 1353599195, https://en.wikipedia.org/w/index.php?title=No-hair_theorem&oldid=1353599195
• W. Israel, Event Horizons in Static Vacuum Space-Times, Phys. Rev. 164 (1967) 1776, https://doi.org/10.1103/PhysRev.164.1776
• W. Israel, Event horizons in static electrovac space-times, Commun. Math. Phys. 8 (1968) 245, https://doi.org/10.1007/BF01645859
• B. Carter, Axisymmetric Black Hole Has Only Two Degrees of Freedom, Phys. Rev. Lett. 26 (1971) 331, https://doi.org/10.1103/PhysRevLett.26.331
• S. Bhattacharya, A. Lahiri, No hair theorems for positive Λ, Phys. Rev. Lett. 99 (2007) 201101, https://arxiv.org/abs/gr-qc/0702006

Motivation

The Yukawa potential (or screened Coulomb potential)

$$V_{\mathrm{Yukawa}}(r) = -g^2\,\frac{e^{-\alpha m r}}{r}$$

was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.

Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.

Setting

Throughout, $g\in\mathbb R$ is the coupling (amplitude) constant, $\alpha>0$ a scaling constant, $m\ge 0$ the mass of the exchanged particle and $r>0$ the radial distance; $1/(\alpha m)$ is the range. The potential is the function

$$V(r) = -g^2\,\frac{e^{-\alpha m r}}{r}.$$

Points of space are $x\in\mathbb R^3$ with Euclidean norm $|x|$, and the potential of a point source at the origin is $x\mapsto V(|x|)$. The Laplacian $\Delta$ is the usual sum of unmixed second partial derivatives on $\mathbb R^3$. For a uniform, infinitesimally thin spherical shell of radius $R$ with total scaling constant $G$, the potential felt by a point of scaling constant $g$ located at $x$ is

$$V_{\mathrm{shell}}(x) = G\,g\;\frac{1}{4\pi}\int_{S^2}\frac{e^{-\alpha m |x-Ru|}}{|x-Ru|}\,d\sigma(u),$$

the average over the unit sphere $S^2$ (uniform surface measure $\sigma$) of the pair interaction.

Formalization targets

Goal — Fourier transform of the Yukawa potential

For $\alpha m>0$ and every $k\in\mathbb R^3$,

$$\int_{\mathbb R^3} e^{-i k\cdot x}\,V(|x|)\,d^3x \;=\; -g^2\,\frac{4\pi}{|k|^2+(\alpha m)^2}.$$

This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator $4\pi/(k^2+(\alpha m)^2)$ times $-g^2$.

Milestones (in the order of the article)

1. Negativity and monotonicity — for $g\neq0$, $V<0$ on $(0,\infty)$ and $V$ is strictly increasing there.
2. Massless limit — for $m=0$, $V(r) = -g^2\cdot\frac1r$ (the Coulomb potential).
3. Screened Poisson equation — $\Delta\,V(|x|) = (\alpha m)^2\,V(|x|)$ for $x\neq0$.
4. Inverse Fourier representation — for $x\ne0$, $V(|x|) = \lim_{\Lambda\to\infty} \frac{-g^2}{(2\pi)^3}\int_{|k|<\Lambda} e^{ik\cdot x}\frac{4\pi}{|k|^2+(\alpha m)^2}\,d^3k$.
5. Born amplitude — $\frac{-2\mu}{\hbar^2 q}\int_0^\infty r\,V(r)\sin(qr)\,dr = \frac{2\mu g^2}{\hbar^2[(\alpha m)^2+q^2]}$ for $q>0$.
6. Momentum transfer — $|\vec p-\vec p'| = 2p\sin(\theta/2)$ when $|\vec p|=|\vec p'|=p$ and $\theta$ is the angle between them.
7. Total cross section — $\frac{4\mu^2g^4}{\hbar^4}\int_0^\pi\frac{2\pi\sin\theta\,d\theta}{[(\alpha m)^2+4p^2\sin^2(\theta/2)]^2} = \frac{4\mu^2g^4}{\hbar^4}\,\frac{4\pi}{(\alpha m)^2[(\alpha m)^2+4p^2]}$.
8. Shell, exterior — for $|x|>R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m|x|}}{|x|}\,\frac{\sinh(\alpha m R)}{\alpha m R}$.
9. Shell, interior — for $0<|x|<R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m R}}{R}\,\frac{\sinh(\alpha m |x|)}{\alpha m |x|}$.

Significance

The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator $-\Delta + (\alpha m)^2$; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.

Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.

Difficulty

The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in $\mathbb R^3$), then evaluating $\int_0^\infty e^{-ar}\sin(kr)\,dr$. The inverse transform is not absolutely convergent — $1/(|k|^2+a^2)$ is not integrable on $\mathbb R^3$ — so the naive Lebesgue statement is false (it would assign the value $0$); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral $\int_0^\infty \frac{k\sin(kr)}{k^2+a^2}dk = \frac{\pi}{2}e^{-ar}$. The shell theorem needs the surface measure on $S^2$ and the Archimedes-type change of variables $u\mapsto |x-Ru|$.

Formalization scope

All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at $r=0$ Lean's division convention gives the junk value $0$, so every statement either restricts to $r>0$ / $x\neq0$ or integrates (where a single point is null). The physical conventions $\alpha>0$, $m\ge0$ (and $m>0$ where the article divides by $\alpha m$) are explicit hypotheses. The Fourier transform uses the convention $\hat V(k)=\int e^{-ik\cdot x}V$, $V=(2\pi)^{-3}\int e^{ik\cdot x}\hat V$; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants $\mu,\hbar$ in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.

Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified $\mathcal O(K^{-7})$ and "$\cdots$" terms), and the $m\to0$ limits of the shell formulas.

Contributions welcome: polar-coordinate integration for radial functions on $\mathbb R^3$, spherical-average lemmas, and the improper integrals above as standalone lemmas.

Selected references

• H. Yukawa, On the interaction of elementary particles, Proc. Phys.-Math. Soc. Japan 17, 48 (1935). https://doi.org/10.11429/ppmsj1919.17.0_48
• D. J. Griffiths, Introduction to Quantum Mechanics, Cambridge University Press (2017), p. 415.
• R. P. Feynman, R. B. Leighton, M. Sands, The Feynman Lectures on Physics, Vol. II, Ch. 28 (1964). https://www.feynmanlectures.caltech.edu/II_28.html
• K. McDonald, A Naïve Estimate of the Coupling Constant in Yukawa Theory (1984/2021). http://kirkmcd.princeton.edu/examples/yukawa.pdf
• Wikipedia, Yukawa potential, revision 1371658231. https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231

Motivation

The Virasoro–Shapiro amplitude is the tree-level scattering amplitude of four tachyons in the closed bosonic string. Together with the Veneziano amplitude for open strings it is historically the first formula of string theory: both were written down around 1968–69 as closed-form guesses with striking properties, before anyone knew they described strings (Veneziano 1968, Virasoro 1969, Shapiro 1970). In David Tong's Cambridge Part III lecture notes on string theory, the amplitude is reduced in Section 6.2.2 to a single integral over the complex plane, and the whole physical content of the answer (the symmetry in the Mandelstam variables, the infinite tower of poles at the string masses, the soft high-energy behaviour) is read off from the closed form of that integral in terms of Euler's Gamma function, eq. (6.11). The evaluation itself is carried out in the Appendix, Section 6.5.

Setting

For complex numbers $a,b$ define the Virasoro–Shapiro integral

$$C(a,b)=\int_{\mathbb C} d^2z\,|z|^{2a-2}\,|1-z|^{2b-2},$$

where, following Tong's convention, $d^2z = 2\,dx\,dy$ for $z=x+iy$ (twice Lebesgue measure on $\mathbb R^2$). Powers of the positive reals $|z|$ and $|1-z|$ are $r^{w}=e^{w\log r}$. The integral converges absolutely exactly when

$$\operatorname{Re}a>0,\qquad \operatorname{Re}b>0,\qquad \operatorname{Re}c>0,\qquad\text{where } a+b+c=1,$$

the three conditions controlling integrability near $z=0$, near $z=1$ and at $z=\infty$ respectively. $\Gamma$ denotes Euler's Gamma function, defined by $\Gamma(z)=\int_0^\infty t^{z-1}e^{-t}\,dt$ for $\operatorname{Re}z>0$ (eq. (6.26)) and continued analytically.

In the physics application $a=1+\alpha' p_2\cdot p_3/2$ and $b=1+\alpha' p_3\cdot p_4/2$ are determined by the tachyon momenta, and the three Gamma-function ratios become $\Gamma(-1-\alpha's/4)/\Gamma(2+\alpha's/4)$ and its $t,u$ analogues (eq. (6.12)).

Formalization targets

Goal: eq. (6.11)

For $a+b+c=1$ with $\operatorname{Re}a,\operatorname{Re}b,\operatorname{Re}c>0$,

$$C(a,b)=\frac{2\pi\,\Gamma(a)\,\Gamma(b)\,\Gamma(c)}{\Gamma(1-a)\,\Gamma(1-b)\,\Gamma(1-c)}.$$

Milestones (Appendix 6.5, in the order of the notes)

1. Eq. (6.27), the Euler Beta integral $\int_0^1 t^{x-1}(1-t)^{y-1}dt=\Gamma(x)\Gamma(y)/\Gamma(x+y)$ (already published on the platform; used as a reference).
2. The Gamma-function representation $|z|^{2a-2}=\Gamma(1-a)^{-1}\int_0^\infty t^{-a}e^{-|z|^2t}\,dt$.
3. The Gaussian reduction of $C(a,b)$ to a double integral over $t,u>0$.
4. The change of variables $t=\alpha\beta$, $u=(1-\beta)\alpha$.
5. The $\alpha$-integral $\int_0^\infty \alpha^{-a-b}e^{-\beta(1-\beta)\alpha}d\alpha=[\beta(1-\beta)]^{a+b-1}\Gamma(1-a-b)$.
6. The Beta-integral form $C(a,b)=\frac{2\pi\Gamma(c)}{\Gamma(1-a)\Gamma(1-b)}\int_0^1(1-\beta)^{a-1}\beta^{b-1}d\beta$.

Significance

The result. Eq. (6.11) is what turns the four-point function (6.10) into the Virasoro–Shapiro amplitude (6.12). Every property Tong extracts in Section 6.2.3 — the manifest $s\leftrightarrow t\leftrightarrow u$ symmetry, the poles at $s=4(n-1)/\alpha'$ reproducing the closed-string mass formula, and the exponential fall-off at high energy — is a property of the Gamma-function expression, not of the raw integral. The same integral (with general exponents) is the basic building block of Coulomb-gas computations in two-dimensional conformal field theory (Dotsenko–Fateev 1984).

Formalizing it. The identity is classical and its proof is elementary but analytically delicate. No machine-checked proof of the complex-plane integral is known to the mission author. A formal proof requires a reusable toolkit: Fubini–Tonelli manipulations of absolutely convergent iterated integrals with complex powers, two-dimensional Gaussian integrals, and a polar/affine change of variables on $(0,\infty)\times(0,1)$. The Beta integral (milestone 1) is already in Mathlib.

Difficulty

Each step of the textbook computation interchanges the order of integration in an integral with integrable but unbounded singularities at $z=0$, $z=1$ and at infinity, so each interchange must be justified by absolute convergence under exactly the three conditions above. The naive approach of applying Fubini directly to the original integrand in Cartesian coordinates does not factor; the proof in the notes instead introduces two auxiliary Gamma-function integrals, making the integral four-dimensional before any variable is integrated out, and the justification of Tonelli for that four-dimensional integrand is the main technical point.

Formalization scope

The integral is TongString.virasoroShapiroIntegral a b, defined as 2 * ∫ z : ℂ, (‖z‖ : ℂ) ^ (2a-2) * (‖1-z‖ : ℂ) ^ (2b-2), the integral being the Bochner integral against Lebesgue measure on $\mathbb C\cong\mathbb R^2$; the factor $2$ implements $d^2z=2\,dx\,dy$. Complex powers are Mathlib's principal-branch cpow applied to non-negative real bases, which agrees with $e^{w\log r}$ for $r>0$ (the point $z=0$, $z=1$ is a null set). The parameters $a,b,c$ are complex; the notes use real Mandelstam-type exponents, which are a special case. Since the Bochner integral of a non-integrable function is $0$ in Lean, every statement carries the convergence hypotheses; with them the integral is a genuine absolutely convergent integral, so the goal cannot be satisfied vacuously. The Gamma function is Mathlib's Complex.Gamma.

Contributions welcome: proofs of any milestone, and general lemmas on iterated integrals over $(0,\infty)^2$ with complex-power weights, which are reusable for other Selberg- and Dotsenko–Fateev-type integrals.

Selected references

• D. Tong, String Theory, Cambridge Part III lecture notes, 2009, Sections 6.2.2 and 6.5. http://www.damtp.cam.ac.uk/user/tong/string.html (arXiv:0908.0333)
• M. A. Virasoro, Alternative constructions of crossing-symmetric amplitudes with Regge behavior, Phys. Rev. 177 (1969) 2309. https://doi.org/10.1103/PhysRev.177.2309
• J. A. Shapiro, Electrostatic analogue for the Virasoro model, Phys. Lett. B 33 (1970) 361. https://doi.org/10.1016/0370-2693(70)90157-8
• J. Polchinski, String Theory, Vol. 1, Cambridge University Press, 1998, Section 6.6.
• Vl. S. Dotsenko, V. A. Fateev, Conformal algebra and multipoint correlation functions in 2D statistical models, Nucl. Phys. B 240 (1984) 312. https://doi.org/10.1016/0550-3213(84)90269-4

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

Motivation

The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric $g_{\mu\nu}$, to its matter–energy content, encoded in the stress–energy tensor $T_{\mu\nu}$:

$$G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu},\qquad \kappa=\frac{8\pi G}{c^4}.$$

They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, $\nabla_\beta T^{\alpha\beta}=0$. For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).

Setting

Everything is written in one coordinate chart. A point is $x\in\mathbb{R}^D$, where $D$ is the spacetime dimension (not fixed to $4$). A 2-tensor field is a matrix-valued function $x\mapsto T_{ab}(x)$. A metric on an open set $U$ is a 2-tensor field $g$ whose components are $C^\infty$ on $U$ and which is symmetric and nondegenerate at each point of $U$; $g^{ab}$ denotes the inverse matrix. Partial derivatives $\partial_a$ are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler $(+\,+\,+)$ convention adopted by the source:

• Christoffel symbols $\Gamma^c_{ab}=\tfrac12g^{cs}(\partial_ag_{sb}+\partial_bg_{sa}-\partial_sg_{ab})$;
• Riemann tensor $R^\mu{}_{\alpha\beta\gamma}=\partial_\beta\Gamma^\mu_{\alpha\gamma}-\partial_\gamma\Gamma^\mu_{\alpha\beta}+\Gamma^\mu_{\sigma\beta}\Gamma^\sigma_{\gamma\alpha}-\Gamma^\mu_{\sigma\gamma}\Gamma^\sigma_{\beta\alpha}$;
• Ricci tensor $R_{\mu\nu}=R^\alpha{}_{\mu\alpha\nu}$, scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$, Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\tfrac12Rg_{\mu\nu}$;
• covariant derivative $\nabla_\lambda T_{\mu\nu}=\partial_\lambda T_{\mu\nu}-\Gamma^\sigma_{\lambda\mu}T_{\sigma\nu}-\Gamma^\sigma_{\lambda\nu}T_{\mu\sigma}$ and divergence $(\operatorname{div}T)_\mu=g^{\nu\lambda}\nabla_\lambda T_{\mu\nu}$, the index-lowered form of $\nabla_\nu T^{\mu\nu}$;
• the field equations on $U$: $G_{\mu\nu}(x)+\Lambda g_{\mu\nu}(x)=\kappa T_{\mu\nu}(x)$ for all $x\in U$.

Formalization targets

Goal: local energy–momentum conservation

For a smooth nondegenerate symmetric metric $g$ on an open $U\subseteq\mathbb{R}^D$, constants $G,c>0$, $\kappa=8\pi G/c^4$, any $\Lambda$, and any $T$ such that the field equations hold on $U$:

$$g^{\beta\lambda}\nabla_\lambda T_{\alpha\beta}=0\quad\text{on }U.$$

Milestones

• Symmetry of the Einstein tensor, $G_{\mu\nu}=G_{\nu\mu}$.
• Metric compatibility, $\nabla_\lambda g_{\mu\nu}=0$.
• The differential Bianchi identity $R^\mu{}_{\alpha[\beta\gamma;\varepsilon]}=0$.
• The contracted Bianchi identity, $G^{\alpha\beta}{}_{;\beta}=0$.
• The trace of the EFE, $R-\tfrac D2R+D\Lambda=\kappa T$.
• Equivalence with the trace-reversed form $R_{\mu\nu}-\tfrac2{D-2}\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac1{D-2}Tg_{\mu\nu})$ for $D\neq2$.
• The vacuum equations $R_{\mu\nu}=\Lambda g_{\mu\nu}/(\tfrac D2-1)$ when $T=0$, $D\neq2$.
• The cosmological term as vacuum stress–energy $T^{(\mathrm{vac})}_{\mu\nu}=-\tfrac\Lambda\kappa g_{\mu\nu}$, with $\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\Lambda/\kappa$.
• Minkowski space $\operatorname{diag}(-1,1,1,1)$ is a vacuum solution.

Significance

Conservation of $T_{\mu\nu}$ is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.

All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.

Difficulty

The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of $g$; without symmetry the identity $g^{\mu\nu}g_{\mu\nu}=D$ fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse $g^{-1}$, and lengthy index bookkeeping with sums over $\operatorname{Fin} D$. Since all objects are total functions, every derivative step must be justified by differentiability on the open set $U$, not taken for granted.

Formalization scope

• Coordinates: $\mathbb{R}^D$ is represented as Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. $D$ is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).
• Regularity: the metric components are $C^\infty$ on the open set $U$; $T$ carries no assumptions, as the field equations determine it on $U$.
• Total-function conventions: the inverse of a singular matrix is $0$ and the derivative of a non-differentiable function is $0$; nondegeneracy on $U$ and openness of $U$ make these junk values irrelevant at points of $U$.
• Divergence is taken on the second index; for symmetric tensors such as $G$ this is the same as the first.
• Not formalized: the Newtonian limit (it rests on approximations), the Einstein–Maxwell system, and the polynomial form.
• Reusable output: coordinate Christoffel/Riemann/Ricci calculus, metric compatibility, Bianchi identities.

Selected references

• Wikipedia, Einstein field equations, revision 1374672993. https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993
• C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman, 1973.
• S. Carroll, Spacetime and Geometry: An Introduction to General Relativity, Addison Wesley, 2004.

Motivation

In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion $R$. Harlow's TASI 2017 lectures (arXiv:1802.01040) review the answer that emerged from quantum error correction: the boundary Hilbert space is a code, bulk effective field theory lives in a code subspace, and the boundary subregion $R$ can reconstruct every bulk operator in its entanglement wedge. The lectures state as their main technical target the theorem that this entanglement wedge reconstruction, the quantum Ryu–Takayanagi (RT) formula with a central area operator, and the JLMS formula (equality of boundary and bulk relative entropies) are mathematically equivalent. All of these statements are finite-dimensional linear algebra, which makes them formalizable now.

Timeline. Almheiri, Dong and Harlow proposed the quantum-error-correction interpretation of AdS/CFT in 2014 (arXiv:1411.7041). Jafferis, Lewkowycz, Maldacena and Suh derived the JLMS relation in 2015 (arXiv:1512.06431), and Dong, Harlow and Wall established the implications between JLMS and reconstruction for factors in 2016 (arXiv:1601.05416). Harlow proved the general three-way equivalence for arbitrary finite-dimensional von Neumann algebras in 2016 (arXiv:1607.03901, Comm. Math. Phys. 2017). The TASI lectures (2017, published 2018) present this theorem as Theorem 5.2.

Setting

All Hilbert spaces are finite-dimensional. The boundary space factorizes as $\mathcal H=\mathcal H_R\otimes\mathcal H_{\overline R}$. A code subspace $\mathcal H_{code}\subseteq\mathcal H$ is described by an isometry $V$ whose columns $|\tilde i\rangle$ are an orthonormal basis of $\mathcal H_{code}$. An operator $O_R$ on $\mathcal H_R$ represents a logical operator $\tilde O$ if $O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle$ and $O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle$ for every code state.

A von Neumann algebra $M$ on $\mathcal H_{code}$ is a set of operators closed under sums, products and adjoints and containing all multiples of the identity; $M'$ is its commutant and $Z_M=M\cap M'$ its center. Every such $M$ is block diagonal, $\mathcal H_{code}=\bigoplus_\alpha\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}$ with $M=\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}$. For a state $\tilde\rho$ with diagonal blocks $p_\alpha\tilde\rho_{r_\alpha\overline r_\alpha}$, the algebraic entropy is $S(\tilde\rho,M)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\tilde\rho_{r_\alpha})$, and the algebraic relative entropy $S(\tilde\rho|\tilde\sigma,M)$ is defined analogously (eqs. (5.16), (5.18)).

Formalization targets

Goal: Theorem 5.2 (entanglement wedge reconstruction theorem)

For $\mathcal H_{code}\subseteq\mathcal H_R\otimes\mathcal H_{\overline R}$ and a von Neumann algebra $M$ on $\mathcal H_{code}$, the following are equivalent:

$$\text{(1) every } \tilde O\in M \text{ is represented on } R \text{ and every } \tilde O'\in M' \text{ on } \overline R;$$ $$\text{(2) } \exists\,\mathcal L_R\in Z_M:\ S(\tilde\rho_R)=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M),\ \ S(\tilde\rho_{\overline R})=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M')\ \ \forall\tilde\rho;$$ $$\text{(3) } S(\tilde\rho_R|\tilde\sigma_R)=S(\tilde\rho|\tilde\sigma,M),\ \ S(\tilde\rho_{\overline R}|\tilde\sigma_{\overline R})=S(\tilde\rho|\tilde\sigma,M')\ \ \forall\tilde\rho,\tilde\sigma.$$

Milestones

• Theorem 4.1: four equivalent characterizations of a correctable erasure of $\overline R$ (operator reconstruction on $R$; $PX_{\overline R}P=\lambda P$; decoupling of a reference system from $\overline R$; the explicit encoding $|\tilde i\rangle=U_R(|i\rangle_{R_1}|\chi\rangle_{R_2\overline R})$).
• Eq. (4.25): the quantum Singleton bound $m\ge\frac{n+k}{2}$ for codes whose accessibility depends only on the number of qudits.
• Theorem 5.1: every von Neumann algebra on a finite-dimensional Hilbert space is a block-diagonal direct sum of factors, with the matching descriptions of $M'$ and $Z_M$.

Significance

Theorem 5.2 turns three separately motivated features of holography into a single mathematical statement. Since the RT formula is independently derived from the gravitational path integral, the theorem implies subregion duality in the entanglement wedge; it also shows that a non-trivial area operator requires an algebra with non-trivial center. Theorem 4.1 is the subsystem-code special case, and Theorem 5.1 is the structure result that gives the algebraic entropies their meaning.

The results are proved in the literature (Harlow 2017 for Theorem 5.2; Theorems 4.1 and 5.1 are standard), but the lectures state Theorem 5.2 without proof, and none of these statements has a machine-checked proof that this mission is aware of. The mission produces formal statements and, eventually, formal proofs of the finite-dimensional structure theory of operator-algebra quantum error correction.

Difficulty

The three conditions live at different levels: (1) is a statement about operators, (2) about von Neumann entropies of single states, and (3) about relative entropies of pairs of states. Passing between them requires control of the full block structure of $M$ relative to the bipartition $R\overline R$, not only of a single factor, and the classical term $\sum_\alpha p_\alpha\log(p_\alpha/q_\alpha)$ of (5.18) couples different blocks, so the general case does not reduce to the factor case treated earlier in the literature. Relative entropies can be infinite (when supports are not nested), so the equalities in (3) are equalities of extended reals and every argument must remain valid at $+\infty$.

Formalization scope

Hilbert spaces are coordinate spaces $\mathbb C^{\iota}$ for finite index types, operators are complex matrices, tensor products are Kronecker products, and $\mathcal H_{code}$ is the image of an isometry $V$ (an operator $O_R$ acts on code states as $O_R\otimes I_{\overline R}$ applied to $V$). States are density matrices (positive semidefinite, trace one). Von Neumann entropy and relative entropy are defined from eigen-decompositions; relative entropy takes values in the extended reals. A von Neumann algebra is a $*$-subalgebra of matrices; the algebraic entropies are computed in a block decomposition $U$ of $M$, which every statement takes as an arbitrary decomposition realizing $M$ (the value does not depend on the choice). The RT identity is stated as an equality of complex numbers. Theorem 4.1 assumes a nonzero code subspace; the Singleton bound assumes $d\ge2$ and $k\ge1$; both conditions are implicit in the lectures and are needed for the statements to be true.

A trivializing reading is excluded: the hypotheses of every statement are satisfiable, and the goal is a full equivalence of three non-trivial conditions rather than any single implication.

Useful reusable infrastructure: partial traces and their interaction with Kronecker products, entropies of block-diagonal states, relative entropy (Klein's inequality and its equality case), and the structure theory of finite-dimensional $*$-algebras of matrices. Contributions of proofs of the individual implications (1)⇒(2), (2)⇒(3), (3)⇒(1) as sketches are welcome.

Selected references

• D. Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002, 2018. https://arxiv.org/abs/1802.01040
• D. Harlow, The Ryu–Takayanagi Formula from Quantum Error Correction, Comm. Math. Phys. 354 (2017) 865–912. https://arxiv.org/abs/1607.03901
• A. Almheiri, X. Dong, D. Harlow, Bulk Locality and Quantum Error Correction in AdS/CFT, JHEP 04 (2015) 163. https://arxiv.org/abs/1411.7041
• D. Jafferis, A. Lewkowycz, J. Maldacena, S. J. Suh, Relative entropy equals bulk relative entropy, JHEP 06 (2016) 004. https://arxiv.org/abs/1512.06431
• X. Dong, D. Harlow, A. C. Wall, Reconstruction of Bulk Operators within the Entanglement Wedge in Gauge-Gravity Duality, Phys. Rev. Lett. 117 (2016) 021601. https://arxiv.org/abs/1601.05416