Theorem 3 (Wall 2013): null generators with decreasing generalized entropy terminate

Proved

WallGSL.null_generator_terminates

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

general-relativitygeneralized-second-law

Theorem 3. Let $(M,g)$ be a time-oriented Lorentzian spacetime ( $C^\infty$ , Hausdorff, second countable) with a generalized entropy $S_{\rm gen}$ . Let $N$ be an achronal null surface with exterior region $X$ , and let $g_0$ be a point at which the fine-grained generalized entropy of $X$ is decreasing: there is a Cauchy surface $\Sigma\ni g_0$ such that for every neighbourhood $U$ of $g_0$ the slice can be pushed forwards in time inside $U$ to $\Sigma'$ with

S_{\rm gen}(\Sigma'\cap X)<S_{\rm gen}(\Sigma\cap X).

Assume the semiclassical approximation holds near $g_0$ (in the form of the comparison principle of Theorem 1 at $g_0$ ) and the fine-grained GSL holds. Then no future-directed null geodesic ray $W$ starting at $g_0$ with infinite affine parameter stays on $N$ forever:

W([a,\infty))\not\subseteq N.

Equivalently, the null generator through $g_0$ must terminate when traced towards the future, either because it exits $N$ or because spacetime is null geodesically incomplete.

This is the thermodynamic half of the singularity theorem: the GSL forbids a surface whose generalized entropy decreases from being a horizon.

Formalization Note Achronality of $N$ is the property of null surfaces (boundaries of past or future sets) that the paper's proof uses when it states that the horizon $H$ lies on or to the past of $N$ .

Preamble

import Definitions.Def_WallGSL_GeneralizedEntropy

open scoped Manifold Topology ContDiff
open Set

Formal statement

namespace WallGSL

/-- Theorem 3 of Wall (2013): if the fine-grained generalized entropy outside the
achronal null surface `N` is decreasing at `g₀`, the semiclassical comparison of
Theorem 1 holds at `g₀`, and the fine-grained GSL holds, then no future-directed null
geodesic ray starting at `g₀` with infinite affine parameter stays on `N` forever. -/
theorem null_generator_terminates
    {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 → ℝ) (N X : Set M) (g₀ : M)
    (hN : st.IsAchronal N)
    (hdec : st.EntropyDecreasingAt Sgen X g₀)
    (hSC : st.TheoremOneComparisonAt Sgen N X g₀)
    (hGSL : st.FineGrainedGSL Sgen)
    (W : ℝ → M) (a : ℝ) (hW : st.IsFutureInfiniteNullRay W a) (hWa : W a = g₀) :
    ¬ (W '' Ici a ⊆ N) := 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 3, pp. 14–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. $E$ , $M$ (Hausdorff, second countable, $C^\infty$ manifold modelled on $E$ ), a time-oriented Lorentzian metric $(g,\tau)$ , an arbitrary function $S_{\rm gen}$ from subsets of $M$ to $\mathbb R$ , subsets $N,X\subseteq M$ , a point $g_0\in M$ , a curve $W:\mathbb R\to M$ and a real number $a$ .

Hypotheses.

$N$ is achronal: no $p,q\in N$ with $p\ll q$ .
The entropy is decreasing at $g_0$ for $X$ : some Cauchy surface $\Sigma\ni g_0$ has, for each neighbourhood $U$ of $g_0$ , 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)$ .
The Theorem-1 comparison holds at $g_0$ for $(N,X)$ (as defined in WallGSL_GeneralizedEntropy: for each observer $W'$ from $a'$ with $R=I^-(W'([a',\infty)))$ , if $N\cap R=\emptyset$ and a future-null geodesic segment from $g_0$ lies in $N\cap\partial R$ , then decreasing at $g_0$ for $X$ implies decreasing at $g_0$ for $R$ ).
The fine-grained GSL holds (for every observer and Cauchy surfaces $\Sigma'\subseteq J^+(\Sigma)$ , $S_{\rm gen}(\Sigma\cap R)\le S_{\rm gen}(\Sigma'\cap R)$ ).
$W$ is a future-infinite null ray from $a$ : a geodesic on $(a,\infty)$ , right-continuous at $a$ , with future-null velocity for all $t>a$ .
$W(a)=g_0$ .

Conclusion. It is not the case that $W(t)\in N$ for all $t\ge a$ .

There is no hypothesis relating $X$ to $N$ , and $N$ is not required to be a null hypersurface beyond being achronal.

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