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

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

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

Loop quantum gravity (LQG) is a proposal for a quantum theory of the gravitational field in which space itself is built from discrete quanta. Its kinematics rests on two mathematical facts that C. Rovelli's review Loop quantum gravity: the first 25 years (Class. Quantum Grav. 28 (2011) 153002, arXiv:1012.4707) singles out. First, the spin–geometry theorem of Penrose, in the extended form based on a theorem of Minkowski (1897): the angular-momentum vectors attached to the links around a node of a spin network, once they satisfy the closure (gauge-invariance) relation, are exactly the data of a flat polyhedron, so every quantum of space carries a geometry (§2.1). Second, the discreteness of geometric spectra: areas take values $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ with half-integer spins $j_n$, with a strictly positive area gap (§2.1, §2.3, §4.3), which the review calls "the most solid result in loop gravity".

Timeline. Minkowski proved the existence and uniqueness of a convex polyhedron with prescribed face normals and areas in 1897. Penrose introduced spin networks and the spin–geometry theorem around 1971. The discreteness of area and volume in LQG was found by Rovelli and Smolin (1995), with the full area spectrum computed by Ashtekar–Lewandowski and others in 1995–1997.

Setting

Work in Euclidean three-space $\mathbb E^3=\mathbb R^3$ with its standard inner product $\langle\cdot,\cdot\rangle$. Given finitely many vectors $u_1,\dots,u_v\in\mathbb E^3$ and real numbers $h_1,\dots,h_v$, the half-space polyhedron is

$$P(u,h)=\{x\in\mathbb E^3:\ \langle u_l,x\rangle\le h_l\ \text{for all } l\},$$

and its $l$-th face is $F_l=P(u,h)\cap\{x:\langle u_l,x\rangle=h_l\}$. The area of a set lying in a plane orthogonal to a nonzero vector $u$ is its two-dimensional Lebesgue measure, computed as the measure of its orthogonal projection onto the plane $u^\perp$. For a nonzero vector $n$, $\hat n=n/\|n\|$ is its direction.

On the quantum side, a node of a spin network with $v$ links carries vectors $\vec L_1,\dots,\vec L_v$ (the left-invariant derivative operators), subject to the closure relation $\sum_l \vec L_l=0$ (eq. (6)). The review's classical content is: the $\vec L_l$ behave as the area-weighted normals of a polyhedron, whose face areas are $|\vec L_l|$ and whose volume (for $v=4$) is given by the triple product (eq. (10)). Spins $j\in\{0,\tfrac12,1,\tfrac32,\dots\}$ label links; the quantity $\sqrt{j(j+1)}$ is the square root of the $SU(2)$ Casimir. The area spectrum (eq. (26)) is the set of numbers $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ over finite families of spins, with $\gamma$ the Barbero–Immirzi parameter, $\hbar$ the reduced Planck constant and $G$ Newton's constant.

Formalization targets

Goal: Minkowski's theorem in the form of the spin–geometry theorem

For nonzero $n_1,\dots,n_v\in\mathbb E^3$ with pairwise distinct directions $\hat n_l$, spanning $\mathbb E^3$, and with $\sum_l n_l=0$:

$$\exists\,h:\ P(\hat n,h)\ \text{bounded, with nonempty interior, and}\ \operatorname{area}(F_l)=\|n_l\|\ \ \forall l,$$

and any two such polyhedra are translates of each other.

Milestones (in the order of the review)

1. Eq. (6), closure: for a bounded polyhedron with nonempty interior and distinct unit normals $u_l$, $\sum_l \operatorname{area}(F_l)\,u_l=0$.
2. Eq. (10), tetrahedron volume: with face area vectors $L_1,L_2,L_3$ of three faces through a vertex, $V^2=\tfrac29\,|L_1\cdot(L_2\times L_3)|$.
3. Eq. (13), area gap: $\min\{\sqrt{j(j+1)}: j\in\{\tfrac12,1,\tfrac32,\dots\}\}=\tfrac{\sqrt3}{2}$.
4. Eq. (18), area gap in physical units: the least positive element of the area spectrum is $8\pi\hbar G\gamma\,\tfrac{\sqrt3}{2}$.
5. Eq. (26), discreteness: for $\gamma,\hbar,G>0$ the area spectrum has only finitely many elements below any bound.

Significance

The goal theorem is the precise mathematical content behind the statement that "the algebraic structure of the momentum operators determines the existence of a metric at each node and therefore equips each quantum of space with a geometry" (§2.1). Its necessity half (milestone 1) is the classical counterpart of the gauge-invariance constraint (6); its sufficiency and uniqueness halves are what allow LQG states to be read as quantum polyhedra and underlie the "twisted geometry" and polyhedral-volume constructions. The spectral milestones encode the review's discrete-geometry claims in the elementary, operator-free form in which they are stated in eqs. (13), (18) and (26).

All statements here are known theorems; none is open. A search of Mathlib (at the revision used to check these statements) found no theory of convex polytopes, facet areas, the Brunn–Minkowski inequality, or Minkowski's theorem for polyhedra.

Difficulty

The necessity direction (closure) is a divergence-theorem or projection argument, but requires relating the facets of an H-described polytope to its boundary. The existence direction of Minkowski's theorem is a variational argument (maximize volume subject to a linear constraint on support numbers) whose difficulty lies in showing that the optimum has all prescribed faces with positive area; uniqueness is classically deduced from the equality case of the Brunn–Minkowski (or Minkowski mixed-volume) inequality. The spectral milestones are elementary.

Formalization scope

Lean represents $\mathbb E^3$ as EuclideanSpace ℝ (Fin 3). A polyhedron is given by a finite family of normals and support numbers (halfspacePolyhedron), faces by polyhedronFace, and face area by planarArea, the Haar (Lebesgue) measure of the orthogonal projection onto the plane orthogonal to the normal, valued in $[0,\infty]$; areas are compared as extended reals so that an infinite area cannot be confused with $0$. Unit normals are obtained as $n/\|n\|$ (unitDir). The cross product is Mathlib's crossProduct transported to EuclideanSpace. Spins are encoded as $k/2$ with $k\in\mathbb N$, and the area spectrum sums over finite multisets of spins.

The goal excludes trivializing readings: the spanning and distinct-direction hypotheses are the classical non-degeneracy conditions of Minkowski's theorem (without them the existence claim is false), and the conclusion demands a bounded polyhedron with nonempty interior, so empty or flat polyhedra do not count. The review's eq. (10) omits numerical constants; the milestone uses the exact Euclidean constant $2/9$. The operator-theoretic statements of the review (spectra of area and volume operators on $L^2(SU(2)^L/SU(2)^N)$) are out of scope; only their stated numerical content is formalized.

Reusable infrastructure: H-polytopes in $\mathbb R^3$, facet areas, the closure identity, and the Brunn–Minkowski equality case. Contributions of general convex-geometry lemmas are welcome.

Selected references

• C. Rovelli, Loop quantum gravity: the first 25 years, Class. Quantum Grav. 28 (2011) 153002. https://doi.org/10.1088/0264-9381/28/15/153002 (arXiv:1012.4707)
• H. Minkowski, Allgemeine Lehrsätze über die konvexen Polyeder, Nachr. Ges. Wiss. Göttingen (1897) 198–219.
• E. Bianchi, P. Doná, S. Speziale, Polyhedra in loop quantum gravity, Phys. Rev. D 83 (2011) 044035. https://arxiv.org/abs/1009.3402
• A. D. Alexandrov, Convex Polyhedra, Springer (2005).

Motivation

In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator $-\Delta + V$: one shows that $V$ is a relatively compact perturbation of $-\Delta$, concludes $\sigma_{ess}(-\Delta + V) = \sigma_{ess}(-\Delta) = [0,\infty)$, and is left with the discrete eigenvalues below zero.

The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.

Setting

Let $\mathfrak H$ be a complex Hilbert space and $A$ a linear operator with domain $\mathfrak D(A) \subseteq \mathfrak H$. For $z \in \mathbb C$, the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $\mathfrak H$ with a bounded inverse. The resolvent set $\rho(A)$ is the set of such $z$, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$.

The discrete spectrum $\sigma_d(A)$ is the set of eigenvalues $z$ of $A$ that are isolated points of $\sigma(A)$ and whose eigenspace $\operatorname{Ker}(A - z)$ is finite dimensional. The essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

A sequence $\psi_n \in \mathfrak D(A)$ with $\|\psi_n\| = 1$, $\langle \varphi, \psi_n \rangle \to 0$ for every $\varphi$ (weak convergence to zero) and $\|(A - z)\psi_n\| \to 0$ is a singular Weyl sequence for $A$ at $z$.

An operator is compact if it maps bounded sets to relatively compact sets; $\mathfrak C(\mathfrak H)$ denotes the compact operators. An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$. $B$ is $A$ bounded if $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\|B\psi\| \le a\|A\psi\| + b\|\psi\|$ on $\mathfrak D(A)$; the infimum of admissible $a$ is the $A$-bound. A symmetric operator $A$ has defect indices $d_\pm(A) = \dim \operatorname{Ran}(A \pm i)^\perp$.

Formalization targets

Goal: Weyl's theorem (Theorem 6.19)

For self-adjoint $A$ and $B$,

$$\exists\, z \in \rho(A) \cap \rho(B):\ R_A(z) - R_B(z) \in \mathfrak C(\mathfrak H) \quad\Longrightarrow\quad \sigma_{ess}(A) = \sigma_{ess}(B).$$

Milestones

• Weyl criterion (Lemma 6.17). For self-adjoint $A$: $z \in \sigma_{ess}(A)$ if and only if a singular Weyl sequence at $z$ exists; if so, it can be chosen orthonormal.
• Compact perturbations (Lemma 6.18). For self-adjoint $A$ and compact self-adjoint $K$, $\sigma_{ess}(A + K) = \sigma_{ess}(A)$, and

$$\sigma_{ess}(A) = \bigcap_{K \in \mathfrak C(\mathfrak H),\, K^* = K} \sigma(A + K).$$

• Independence of $z$ (Lemma 6.21, first part). If $R_A(z) - R_B(z)$ is compact for one $z \in \rho(A) \cap \rho(B)$, it is compact for all such $z$.
• Self-adjoint extensions (Theorem 6.20). If $A$ is symmetric with $d_+(A) = d_-(A) < \infty$, all self-adjoint extensions of $A$ have the same essential spectrum.
• Relative compactness is infinitesimal (Lemma 6.22). For self-adjoint $A$, a relatively compact $K$ has $A$-bound $0$.
• Stability of relative compactness (Lemma 6.23). If $A$ is self-adjoint, $B$ symmetric with $A$-bound less than one, and $K$ relatively compact with respect to $A$, then $K$ is relatively compact with respect to $A + B$.

Significance

The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields $\sigma_{ess}(A + K) = \sigma_{ess}(A)$ for every relatively compact symmetric $K$; Lemma 6.23 extends this to perturbations of the form $B + K$. These are the inputs to the HVZ theorem for $N$-body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in $\sigma_{ess}$ in concrete examples.

Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, $\sigma_d$, $\sigma_{ess}$, singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.

Difficulty

The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections $P_A((\lambda - \varepsilon, \lambda + \varepsilon))$ and spectral measures $\mu_{\psi_n}$, and his characterization (6.27)–(6.28) of $\sigma_{ess}$ by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of $\sigma_{ess}$ used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of $\sigma(A) \setminus \sigma_d(A)$ carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.

A second difficulty is domain bookkeeping. $A + K$, $A + B$, $K R_A(z)$ and $R_{A+B}(z)$ all involve unbounded operators with different domains, and identities such as the second resolvent formula $K R_{A+B}(z) = K R_A(z)(\mathbb I - B R_{A+B}(z))$ must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.

Formalization scope

The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of $A - z$ of p. 73 (IsResolventAt), and $\rho(A)$, $\sigma(A)$ are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one $z \in \rho(A) \cap \rho(B)$" is an existential over $z$ and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. $A + K$ for bounded $K$ is K +ᵥ A (domain $\mathfrak D(A)$); $A + B$ for unbounded $B$ is the LinearPMap sum with domain $\mathfrak D(A) \cap \mathfrak D(B)$. The $A$-bound is valued in $[0,\infty]$ and is $\infty$ for an operator that is not $A$ bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.

No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without $f(A)$. For this reason the second half of Lemma 6.21, $f(A) - f(B) \in \mathfrak C(\mathfrak H)$ for $f \in C_\infty(\mathbb R)$, and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.

A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in $\sigma(A)$" and "finite-dimensional eigenspace", so $\sigma_{ess}$ is neither empty nor all of $\sigma(A)$ by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside $\rho(A)$.

A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, $\sigma_{ess}$, relative compactness and $A$-bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Section 6.4. https://doi.org/10.1090/gsm/099
• H. Weyl, Über beschränkte quadratische Formen, deren Differenz vollstetig ist, Rendiconti del Circolo Matematico di Palermo 27 (1909), 373–392. https://doi.org/10.1007/BF03019655
• M. Reed and B. Simon, Methods of Modern Mathematical Physics IV: Analysis of Operators, Academic Press, 1978, Section XIII.4.
• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer, 1980, Section IV.5. https://doi.org/10.1007/978-3-642-66282-9

Motivation

Classical statistical mechanics describes a particle by a probability density on phase space; quantum mechanics replaces this by a wavefunction, and the uncertainty principle forbids any honest probability interpretation of simultaneous position and momentum. In 1932, Eugene Wigner introduced the transform that has become the standard way of placing quantum states on classical phase space anyway: a quasiprobability distribution $W(x, p)$, defined by an explicit integral formula, whose marginals reproduce the Born position and momentum distributions of the wavefunction (Wigner 1932). Unlike a probability density, $W$ generally takes negative values, and this negativity is the standard marker of genuinely quantum behavior — of interference — in quantum optics, quantum information, and the study of the quantum-to-classical transition.

The central question about the probabilistic character of $W$ is: which quantum states have an everywhere nonnegative Wigner function? Hudson's theorem (1974) gives the complete answer in one dimension: only Gaussian wave packets (Hudson 1974). This mission formalizes the definition, the basic properties, and the positivity characterization of the Wigner function, following the source text, the Wikipedia article Wigner quasiprobability distribution (oldid 1376057304).

Timeline of the key results:

• 1932 — E. Wigner introduces the distribution to study quantum corrections to thermodynamic equilibrium (Physical Review 40, 749).
• 1946 — H. J. Groenewold computes the Wigner function of the $m$-th Fock (number) state, this mission's key worked example (Physica 12, 405).
• 1949 — J. E. Moyal recognizes $W$ as the moment-generating functional of quantum mechanics in phase space (Proc. Camb. Phil. Soc. 45, 99).
• 1974 — R. L. Hudson proves that Gaussian pure states are the only pure states with nonnegative Wigner function in one dimension (Rep. Math. Phys. 6, 249).
• 1983 — F. Soto and P. Claverie extend the characterization to arbitrary dimension via the Segal–Bargmann transform (J. Math. Phys. 24, 97).

Setting

A wavefunction is a function $\psi : \mathbb{R} \to \mathbb{C}$, and $\hbar > 0$ denotes the reduced Planck constant. The Wigner function of $\psi$ at the phase-space point $(x, p) \in \mathbb{R}^2$ is

$$W(x, p) = \frac{1}{\pi \hbar} \int_{-\infty}^{\infty} \overline{\psi(x+y)}\, \psi(x-y)\, e^{\,2ipy/\hbar}\, dy,$$

a Lebesgue (Bochner) integral over $y$. The Lean development factors this into three definitions mirroring the formula: the integrand (Wigner.wignerIntegrand), the integral (Wigner.wignerIntegral), and the Wigner function itself (Wigner.wigner), defined as the real part of the integral divided by $\pi\hbar$; that the discarded imaginary part vanishes is itself milestone 1. The Fock states of the harmonic oscillator enter through the physicists' Hermite polynomials $H_m$ and the ordinary Laguerre polynomials $L_m$, defined by their standard three-term recurrences, and the normalized $m$-th Hermite function

$$u_m(x) = (2^m m!)^{-1/2}\, \pi^{-1/4}\, H_m(x)\, e^{-x^2/2}.$$

Formalization targets

Goal — Hudson's theorem

$$\int_{\mathbb{R}} |\psi|^2 = 1 \ \text{ and }\ W_\psi \ge 0 \text{ on } \mathbb{R}^2 \ \Longrightarrow\ \exists\, a, b, c \in \mathbb{C},\ \operatorname{Re} a > 0,\ \psi = e^{-ax^2+bx+c} \ \text{a.e.}$$

This is exactly the source's statement of Hudson's theorem; nothing is left unfixed. The mission is complete when the goal is proved.

Milestones

The milestone list is the source's property list, ordered as the attack path: (1) reality of the defining integral; (2) the position marginal $\int W\, dp = |\psi(x)|^2$; (3) the total integral $\iint W = \int |\psi|^2$; (4) Groenewold's closed formula for the Fock states; (5) a concrete negativity witness, the first excited Fock state at the origin; (6) the pointwise bound $|W| \le 2/h$; (7) the converse of Hudson's theorem, that Gaussian pure states have nonnegative Wigner function.

Significance

The result itself. Hudson's theorem draws the exact boundary between the classical and the quantum in phase space: Gaussian states — coherent and squeezed states — are precisely the pure states that can be described by an honest phase-space probability density. This is used in quantum optics as a nonclassicality criterion, in tomography and state-reconstruction theory, and in the study of the quantum-to-classical transition: negativity of $W$ is shielded by the uncertainty principle (negative regions cannot extend beyond a few $\hbar$) and disappears in the classical limit, as the source emphasizes.

What formalizing it adds. The Wigner transform and this circle of ideas are absent from current Mathlib, so the mission builds the foundations itself: the integral transform and its basic identities (reality, marginals, normalization, boundedness), the Hermite/Laguerre recurrences and Groenewold's Fock-state formula, and finally Hudson's theorem with its converse. All of these are reusable well beyond the mission — for quantum optics, for the Wigner–Ville time–frequency distribution used in signal analysis, and for the wider phase-space formulation of quantum mechanics (Moyal brackets, star products). These are known results: this is formalization of known mathematics, not new mathematics, and no machine-checked proof of Hudson's theorem exists in Mathlib today.

Difficulty

The naive approach to Hudson's theorem is doomed from the start, and solvers should know it: since the Husimi $Q$ function (a Gaussian smoothing of $W$) is positive for every quantum state, no smoothing or positivity-of-convolution argument can extract any information from $W \ge 0$. The known route (Soto–Claverie) is: $W \ge 0$ everywhere forces the Husimi function strictly positive everywhere; the Husimi function is the squared modulus of the Segal–Bargmann transform $F$ of $\psi$, so $F$ is a zero-free entire function; hence $F = e^g$ for some entire $g$, and square-integrability of $F$ against a Gaussian measure forces $g$ to have at most quadratic growth, hence to be a quadratic polynomial; inverting the Segal–Bargmann transform then exhibits $\psi$ as a Gaussian. The hard Lean steps are the growth-to-polynomial (Liouville-type) step, the inversion of the transform, and, for the milestone properties, the Fubini and Fourier-inversion machinery. Mathlib contains the raw harmonic analysis (Fourier inversion for Schwartz functions) but none of the assembled phase-space layer.

Formalization scope

• Integrals are Bochner integrals with respect to Lebesgue measure on $\mathbb{R}$; statements carry the integrability or regularity hypotheses under which the source's displayed integrals exist.
• $\hbar$ is an explicit real parameter, and every statement assumes $0 < \hbar$ (the standing convention of the source). The Fock-state section uses the source's dimensionless units, i.e. $\hbar = 1$.
• The Wigner function is defined as the real part of the defining integral divided by $\pi\hbar$; milestone 1 proves the imaginary part vanishes, so this is the same function as the source's.
• Pure states are encoded by the normalization $\int |\psi|^2 = 1$.
• The conclusion of Hudson's theorem holds only up to modification of $\psi$ on a Lebesgue-null set ($W$ is insensitive to null-set changes of $\psi$), so the goal states almost-everywhere equality; this is the faithful reading of "the wavefunction must have the form".
• The Fock states are normalized: the source's displayed $u_m = \pi^{-1/4} H_m e^{-x^2/2}$ omits the factor $(2^m m!)^{-1/2}$ that its Fock-state formula requires; the definition includes it, since Groenewold's formula is stated for the normalized number states $|m\rangle = (a^\dagger)^m/\sqrt{m!}\,|0\rangle$.
• There is no trivializing encoding: Hudson's hypothesis ranges over all normalized wavefunctions, and the conclusion is not weakened beyond the almost-everywhere reading.

Infrastructure contributed and reusable beyond this mission: hermiteP, laguerreL, fockState, wignerIntegrand, wignerIntegral, wigner. Welcome additional contributions: the momentum marginal, the state-overlap formula (Property 6), Galilei covariance (Property 4), and harmonic-oscillator time evolution, as further theorems in the same namespace.

Selected references

• E. P. Wigner, On the quantum correction for thermodynamic equilibrium, Physical Review 40(5), 749–759, 1932. https://doi.org/10.1103/PhysRev.40.749
• H. J. Groenewold, On the principles of elementary quantum mechanics, Physica 12(7), 405–460, 1946. https://doi.org/10.1016/S0031-8914(46)80059-4
• J. E. Moyal, Quantum mechanics as a statistical theory, Mathematical Proceedings of the Cambridge Philosophical Society 45(1), 99–124, 1949. https://doi.org/10.1017/S0305004100000487
• R. L. Hudson, When is the Wigner quasi-probability density non-negative?, Reports on Mathematical Physics 6(2), 249–252, 1974. https://doi.org/10.1016/0034-4877(74)90007-X
• F. Soto and P. Claverie, When is the Wigner function of multidimensional systems nonnegative?, Journal of Mathematical Physics 24, 97–100, 1983.
• Source text: Wikipedia, Wigner quasiprobability distribution (oldid 1376057304). https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution

Motivation

The AdS/CFT correspondence (Maldacena 1997) relates quantum gravity on anti-de Sitter (AdS) space to a conformal field theory (CFT) living on its timelike boundary. Gubser–Klebanov–Polyakov and Witten gave the CFT-from-AdS direction of the dictionary: CFT correlators are computed from bulk Green functions. Giddings (PRL 83, 2707, 1999) supplies an entry in the reverse direction. Because AdS confines particles and has no ordinary asymptotic states, a flat-space S matrix does not exist; the paper defines a boundary S matrix from in/out states built out of wave packets incident from the boundary, derives an LSZ-type reduction formula (eq. 42), and concludes that the boundary S matrix equals the boundary CFT correlator (eqs. 44–45).

Every step of that argument rests on the classical theory of the free Klein–Gordon field on global AdS: the parameters $h_\pm,\nu$ (eq. 4), the discrete normalizable spectrum $\omega_{nl}=2h_++2n+l$ with modes behaving like $(\cos r)^{2h_+}$ at the boundary (eqs. 5–7), the non-normalizable modes behaving like $(\cos r)^{2h_-}$ (eqs. 8–9), and the boundary limit (eqs. 19–20) that fixes the normalization $2\nu$ of the bulk–boundary propagator.

Setting

Fix an integer $d\ge 2$, an AdS radius $R>0$ and a scalar mass $m\in\mathbb R$. Global $\mathrm{AdS}_{d+1}$ has metric (eq. 2)

$$ds^2=R^2\sec^2 r\,\bigl(-dt^2+dr^2+\sin^2 r\,d\Omega_{d-1}^2\bigr),\qquad 0\le r<\tfrac\pi2 .$$

Define (eq. 4)

$$\nu=\tfrac12\sqrt{d^2+4m^2R^2},\qquad 2h_\pm=\tfrac d2\pm\nu .$$

A mode $\phi=e^{-i\omega t}Y_{l\vec m}(\Omega)\chi(r)$, with $Y_{l\vec m}$ a spherical harmonic on $S^{d-1}$, solves the free equation $(\Box-m^2)\phi=0$ (eq. 3) exactly when the radial profile $\chi$ satisfies, on $0<r<\pi/2$,

$$\chi''+\frac{d-1}{\sin r\cos r}\chi'+\omega^2\chi-\frac{l(l+d-2)}{\sin^2 r}\chi-\frac{m^2R^2}{\cos^2 r}\chi=0 .$$

A normalizable mode is a nonzero $C^2$ solution that is bounded as $r\to0$ (regular at the centre of AdS) and has finite Klein–Gordon norm, i.e. $\int_0^{\pi/2}\tan^{d-1}r\,\chi(r)^2\,dr<\infty$. The explicit modes of eq. (5) are

$$\chi_{nl}(r)=\sin^l r\,(\cos r)^{2h_+}\,P_n^{(l+d/2-1,\;\nu)}(\cos 2r),$$

with $P_n^{(\alpha,\beta)}$ the Jacobi polynomial, and the eigenfrequencies of eq. (7) are $\omega_{nl}=2h_++2n+l$.

Formalization targets

Goal: the normalizable spectrum (eqs. 3–7)

For every $\omega\in\mathbb R$, $l\in\mathbb N$ and radial profile $\chi$,

$$\chi \text{ is a normalizable mode at }(\omega,l)\iff \exists n\in\mathbb N:\ |\omega|=\omega_{nl}\ \text{and}\ \chi=c\,\chi_{nl}\text{ on }(0,\tfrac\pi2)\text{ for some }c\neq0 .$$

Milestones

1. Eq. (4): $2h_\pm$ are the two roots of $\Delta(\Delta-d)=m^2R^2$, and $2h_+-2h_-=2\nu$.
2. Eqs. (5), (7): $\chi_{nl}$ solves the radial equation at $\omega=\omega_{nl}$.
3. Eq. (6): $\chi_{nl}(r)/(\cos r)^{2h_+}\to k_{nl}\neq0$ as $r\to\pi/2$.
4. Eq. (5): $\chi_{nl}$ is a normalizable mode at $(\omega_{nl},l)$.
5. Eqs. (8)–(9): for $|\omega|$ outside the spectrum there is a solution regular at $r=0$ with $\chi(r)/(\cos r)^{2h_-}\to1$.
6. Eqs. (19)–(20): $\displaystyle\lim_{r\to\pi/2}(\tan r)^{d-1}\bigl[(\cos r)^{2h_-}\overleftrightarrow{\partial_r}(\cos r)^{2h_+}\bigr]=-2\nu$.
7. Eqs. (12), (33): $\Delta_b>\Delta\Rightarrow(\cos r)^{\Delta_b-\Delta}\to0$.
8. Eqs. (23), (42)–(44): given Witten's formula (43), the LSZ expression (42) built from the wave packets (23) equals $\int\prod_a[db_a\,f_a(b_a)/Z_a]\,\langle T\prod_a\mathcal O(b_a)\rangle$.

Significance

The goal is the precise mathematical content behind the paper's statement that free solutions "exist at arbitrary frequency but are only normalizable for a discrete set of frequencies". This spectrum is what makes the boundary operators $a_{\omega l\vec m}$ of eq. (25) act as creation and annihilation operators (eqs. 27–29), and the boundary exponents $2h_\pm$ and the constant $2\nu$ determine the normalizations in eqs. (20), (21), (28) and (29). The physics derivation of eqs. (28)–(42) is not rigorous mathematics; milestone 8 isolates the final step from (42)–(43) to (44), which is an exact identity about integral kernels.

The radial results are classical (the paper attributes the explicit solutions to Balasubramanian–Kraus–Lawrence). This mission asks for machine-checked proofs of these results, together with the reusable Jacobi-polynomial and boundary-asymptotics infrastructure they require.

Difficulty

Verifying that $\chi_{nl}$ solves the equation is a computation. The goal's converse direction is the hard part: one must show that a solution regular at $r=0$ can have finite Klein–Gordon norm only when $|\omega|$ equals some $\omega_{nl}$, and that it is then unique up to a scalar. This requires controlling both regular singular points $r=0$ and $r=\pi/2$ of the radial equation, including the resonant cases where $2\nu$ or $l+d/2-1$ is an integer and logarithms appear. Since $d\ge2$ forces $\nu\ge1$, the $(\cos r)^{2h_-}$ branch is never square-integrable, so the second quantization available for $0<\nu<1$ does not arise.

Formalization scope

• $d$ is a natural number with $d\ge2$; $m,R$ are real with $R>0$; $l,n$ are natural numbers; $\omega$ is real and only $|\omega|$ matters.
• Radial profiles are real-valued functions $\mathbb R\to\mathbb R$; only their values on $(0,\pi/2)$ enter any definition. Complex modes reduce to their real and imaginary parts.
• Regularity at the origin is encoded as boundedness of $|\chi|$ on $(0,\pi/4]$. Finite Klein–Gordon norm is integrability of $\tan^{d-1}r\,\chi(r)^2$ on $(0,\pi/2)$.
• The Jacobi polynomial is defined by the explicit finite sum with generalized binomial coefficients. Powers of $\cos r$ with real exponents use Real.rpow; $\cos r>0$ on the relevant range.
• Nontriviality ($\chi\neq0$ somewhere) is part of the definition of a normalizable mode, so the zero function never counts.
• Milestone 8 takes the LSZ right-hand side (42) as the definition of the boundary S matrix and Witten's relation (43) as a hypothesis, with joint integrability of the integrand. In- and out-packets are listed together, and the plane-wave limit (45) is not formalized.

Selected references

• S. B. Giddings, Boundary S matrix and the anti–de Sitter space to conformal field theory dictionary, Phys. Rev. Lett. 83, 2707 (1999). https://doi.org/10.1103/PhysRevLett.83.2707
• V. Balasubramanian, P. Kraus, A. Lawrence, Bulk vs. boundary dynamics in anti-de Sitter spacetime, Phys. Rev. D 59, 046003 (1999). https://arxiv.org/abs/hep-th/9805171
• E. Witten, Anti de Sitter space and holography, Adv. Theor. Math. Phys. 2, 253 (1998). https://arxiv.org/abs/hep-th/9802150
• J. Maldacena, The large N limit of superconformal field theories and supergravity, Adv. Theor. Math. Phys. 2, 231 (1998). https://arxiv.org/abs/hep-th/9711200
• S. S. Gubser, I. Klebanov, A. Polyakov, Gauge theory correlators from non-critical string theory, Phys. Lett. B 428, 105 (1998). https://arxiv.org/abs/hep-th/9802109