Theorem 4 (Wall 2013): the GSL implies a quantum singularity theorem

Open

WallGSL.quantum_singularity_theorem

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

general-relativitygeneralized-second-lawsingularity-theorem

Theorem 4 (quantum singularity theorem). Let $(M,g)$ be a time-oriented Lorentzian spacetime, $C^\infty$ , Hausdorff and second countable, and let $S_{\rm gen}$ be a generalized entropy assigning a real number to every region of $M$ . Assume:

$M$ is globally hyperbolic: no closed timelike curves, and $J^+(p)\cap J^-(q)$ is compact for all $p,q$ ;
$T$ is a quantum trapped surface: $T$ is the nonempty compact boundary, inside a connected Cauchy surface $\Sigma$ , of a relatively open exterior region $\mathrm{Ext}\subseteq\Sigma$ with noncompact closure, and the generalized entropy outside the null surface $N$ shot outwards and to the future from $T$ is decreasing at every point of $T$ ;
the semiclassical approximation holds near $T$ , in the form of the comparison principle of Theorem 1 at every point $g_0\in T$ , comparing $N$ against causal horizons;
the fine-grained GSL holds: for every observer $W$ and Cauchy surfaces $\Sigma'$ nowhere to the past of $\Sigma$ ,

S_{\rm gen}(\Sigma'\cap I^-(W))\ \ge\ S_{\rm gen}(\Sigma\cap I^-(W)).

Then

M \text{ is not null geodesically complete,}

i.e. there is a singularity somewhere.

This is the quantum analogue of Penrose's singularity theorem, with the null energy condition replaced by the generalized second law. It is the main result of the paper and the goal of this mission.

Formalization Note The generalized entropy is an arbitrary function Sgen : Set M → ℝ; all physical input is in hypotheses 2–4 (see the definition files). Hausdorffness and second countability are the field's standing conventions for spacetimes.

Preamble

import Definitions.Def_WallGSL_GeneralizedEntropy

open scoped Manifold Topology ContDiff
open Set

Formal statement

namespace WallGSL

/-- Theorem 4 of Wall (2013): a globally hyperbolic spacetime containing a quantum
trapped surface `T`, near which the semiclassical approximation holds, and in which the
fine-grained GSL holds, is not null geodesically complete. -/
theorem quantum_singularity_theorem
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    {M : Type*} [TopologicalSpace M] [T2Space M] [SecondCountableTopology M]
    [ChartedSpace E M] [IsManifold 𝓘(ℝ, E) ∞ M]
    (st : LorentzianMetric E M) (Sgen : Set M → ℝ) (S T Ext : Set M)
    (hGH : st.IsGloballyHyperbolic)
    (hT : st.IsQuantumTrappedSurface Sgen S T Ext)
    (hSC : ∀ g₀ ∈ T, st.TheoremOneComparisonAt Sgen
      (st.outgoingNullSurface S T Ext) (st.outgoingExterior S Ext) g₀)
    (hGSL : st.FineGrainedGSL Sgen) :
    ¬ st.IsNullGeodesicallyComplete := by sorry

end WallGSL

Source

A. C. Wall, The generalized second law implies a quantum singularity theorem, Class. Quantum Grav. 30 (2013) 165003, https://doi.org/10.1088/0264-9381/30/16/165003, §3.2, Theorem 4, p. 15

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind

Provenance note — this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It is therefore not independent testimony and must not be mistaken for a blind audit; reviewers should treat it as the drafter's own literal reading of the code and compare it against the source themselves.

Data. A finite-dimensional real inner product space $E$ ; a topological space $M$ that is Hausdorff and second countable, with charts into $E$ forming a $C^\infty$ manifold structure; a time-oriented Lorentzian metric $(g,\tau)$ on $M$ in the sense of WallGSL_Spacetime; an arbitrary function $S_{\rm gen}$ from subsets of $M$ to $\mathbb R$ ; and three subsets $S,T,\mathrm{Ext}\subseteq M$ .

Hypotheses.

$M$ is globally hyperbolic: there is no $p$ with $p\ll p$ , and $J^+(\{p\})\cap J^-(\{q\})$ is compact for all $p,q$ .
$(S_{\rm gen},S,T,\mathrm{Ext})$ is a quantum trapped surface: $S$ is a Cauchy surface (met exactly once by every inextendible timelike curve) and is connected; $\mathrm{Ext}\subseteq S$ and $\mathrm{Ext}=V\cap S$ for an open $V$ ; $\overline{\mathrm{Ext}}$ is not compact; $T=(\overline{\mathrm{Ext}}\cap S)\setminus\mathrm{Ext}$ , nonempty and compact; and for each $g_0\in T$ there is a Cauchy surface $\Sigma\ni g_0$ such that every neighbourhood $U$ of $g_0$ admits a Cauchy surface $\Sigma'$ with $\Sigma'\setminus U=\Sigma\setminus U$ , $\Sigma'\subseteq J^+(\Sigma)$ and $S_{\rm gen}(\Sigma'\cap X)<S_{\rm gen}(\Sigma\cap X)$ , where $X=\big(\overline{I^+(S\setminus\mathrm{Ext})}\big)^c$ .
For every $g_0\in T$ , the Theorem-1 comparison holds at $g_0$ for the pair $(N,X)$ with $N=\big(\partial I^+(S\setminus\mathrm{Ext})\setminus(S\setminus\mathrm{Ext})\big)\cup T$ : for every observer $W$ from $a$ (future-infinite timelike worldline or future-infinite null ray), with $R=I^-(W([a,\infty)))$ , if $N\cap R=\emptyset$ and some future-null geodesic segment $\gamma([s,b))$ starting at $\gamma(s)=g_0$ lies in $N\cap\partial R$ , then "entropy decreasing at $g_0$ for $X$ " implies "entropy decreasing at $g_0$ for $R$ ".
Fine-grained GSL: for every observer $W$ from $a$ , with $R$ as above, and Cauchy surfaces $\Sigma,\Sigma'$ with $\Sigma'\subseteq J^+(\Sigma)$ : $S_{\rm gen}(\Sigma\cap R)\le S_{\rm gen}(\Sigma'\cap R)$ .

Conclusion. $M$ is not null geodesically complete: there exist $\gamma$ and $a<b$ such that $\gamma$ is a geodesic on $(a,b)$ with nonzero null velocity throughout, and no geodesic defined on all of $\mathbb R$ agrees with $\gamma$ on $(a,b)$ .

The dimension of $E$ is unrestricted. If $E=\{0\}$ , no metric with $g(\tau,\tau)<0$ exists. If $\dim E=1$ there are no nonzero null vectors, so null geodesic completeness holds trivially and the conclusion is false; in that case the theorem asserts that the hypotheses cannot all hold. No condition ties $S_{\rm gen}$ to the geometry beyond hypotheses 2–4.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph