Generalized entropy, fine-grained GSL and quantum trapped surfaces

Definition

WallGSL_GeneralizedEntropy

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

black-hole-thermodynamicsgeneral-relativitygeneralized-second-law

This definition file encodes the thermodynamic notions of Wall (2013): the generalized entropy, the fine-grained generalized second law, the semiclassical comparison principle of Theorem 1, and quantum trapped surfaces. It builds on WallGSL_Spacetime.

The fine-grained generalized entropy $S_{\rm gen}=A/4\hbar G+Q+S_{\rm out}$ has no rigorous definition, so it is an arbitrary function $S_{\rm gen}:\mathcal P(M)\to\mathbb R$ , read as the generalized entropy of (the part of a slice lying in) a region.

Forward deformation. $\Sigma'$ is obtained from a Cauchy surface $\Sigma$ by pushing it forwards inside $U$ if $\Sigma'$ is a Cauchy surface, $\Sigma'\setminus U=\Sigma\setminus U$ , and $\Sigma'\subseteq J^+(\Sigma)$ .
Decreasing generalized entropy at $g_0$ (Theorem 3's sense) of an exterior region $X$ : there is a Cauchy surface $\Sigma\ni g_0$ such that for every neighbourhood $U$ of $g_0$ there is a forward deformation $\Sigma'$ of $\Sigma$ inside $U$ with $S_{\rm gen}(\Sigma'\cap X)<S_{\rm gen}(\Sigma\cap X)$ .
Observer: a future-infinite timelike worldline, or a future-infinite null ray (§2.2).
Fine-grained GSL (eq. (10)): for every observer $W$ and Cauchy surfaces $\Sigma,\Sigma'$ with $\Sigma'\subseteq J^+(\Sigma)$ ,

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

Theorem 1 comparison at $g_0$ for a null surface $N$ with exterior $X$ : whenever an observer's horizon $H=\partial I^-(W)$ satisfies $N\cap I^-(W)=\emptyset$ and a future-directed null geodesic segment starting at $g_0$ lies on $N\cap H$ , decreasing generalized entropy of $X$ at $g_0$ implies decreasing generalized entropy of $I^-(W)$ at $g_0$ .
Outgoing null surface of $T=\partial_\Sigma\mathrm{Ext}$ : $N=\big(\partial I^+(\Sigma\setminus\mathrm{Ext})\setminus(\Sigma\setminus\mathrm{Ext})\big)\cup T$ , with exterior $\big(\overline{I^+(\Sigma\setminus\mathrm{Ext})}\big)^{c}$ .
Quantum trapped surface (§3.2): $\Sigma$ is a connected Cauchy surface, $\mathrm{Ext}\subseteq\Sigma$ is relatively open with noncompact closure, $T=(\overline{\mathrm{Ext}}\cap\Sigma)\setminus\mathrm{Ext}$ is nonempty and compact, and the generalized entropy of the exterior of $N$ is decreasing at every $g_0\in T$ .

Formalization Note Item 5 is the formal stand-in for "the semiclassical approximation is valid near $g_0$ ": in the paper the comparison is derived (Theorem 1) from the semiclassical expansion, which has no rigorous formulation. "Decreasing" is strict, unlike the $\le$ in eq. (33), because with $\le$ a constant $S_{\rm gen}$ would count as decreasing everywhere while satisfying the GSL.

Definition code

import Definitions.Def_WallGSL_Spacetime

/-!
# Generalized entropy, the generalized second law, and quantum trapped surfaces

Definition layer (part 2) for the formalization of
A. C. Wall, *The generalized second law implies a quantum singularity theorem*,
Class. Quantum Grav. 30 (2013) 165003, §2.2 and §3.

The fine-grained generalized entropy `S_gen = A/(4ħG) + Q + S_out` of the paper has no
rigorous mathematical definition, so it is modelled abstractly as an arbitrary function
`Sgen : Set M → ℝ` assigning a generalized entropy to (the part of a time slice lying in)
a region of spacetime.  All physical input about it enters through explicit hypotheses:
the fine-grained GSL (eq. (10)) and, near the relevant points, the comparison principle
of Theorem 1 (which is the paper's consequence of the semiclassical approximation).
-/

open scoped Manifold Topology ContDiff
open Set Filter

namespace WallGSL

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {M : Type*} [TopologicalSpace M] [ChartedSpace E M] [IsManifold 𝓘(ℝ, E) ∞ M]

namespace LorentzianMetric

variable (st : LorentzianMetric E M)

/-- `S'` is obtained from the Cauchy surface `S` by pushing it forwards in time inside
`U`: `S'` is again a Cauchy surface, it agrees with `S` outside `U`, and it lies in the
causal future of `S` ("nowhere to the past of `S`"). -/
def IsForwardDeformation (S S' U : Set M) : Prop :=
  st.IsCauchySurface S' ∧ S' \ U = S \ U ∧ S' ⊆ st.causalFuture S

/-- The generalized entropy of the exterior region `X` (of some null surface) is
decreasing at the point `g₀`, in the sense of Theorem 3 of the paper: there is a Cauchy
surface `S` through `g₀` such that, for every neighbourhood `U` of `g₀`, `S` can be pushed
forwards in time inside `U` to a Cauchy surface `S'` with
`Sgen (S' ∩ X) < Sgen (S ∩ X)`. -/
def EntropyDecreasingAt (Sgen : Set M → ℝ) (X : Set M) (g₀ : M) : Prop :=
  ∃ S : Set M, st.IsCauchySurface S ∧ g₀ ∈ S ∧
    ∀ U ∈ 𝓝 g₀, ∃ S' : Set M, st.IsForwardDeformation S S' U ∧ Sgen (S' ∩ X) < Sgen (S ∩ X)

/-- An "observer" in the sense of §2.2 of the paper, starting at parameter `a`: either a
future-infinite timelike worldline, or a future-directed null ray whose affine parameter
is infinite to the future. -/
def IsFutureObserver (W : ℝ → M) (a : ℝ) : Prop :=
  st.IsFutureInfiniteTimelike W a ∨ st.IsFutureInfiniteNullRay W a

/-- The fine-grained generalized second law, eq. (10) of the paper: for every observer
`W` with future causal horizon `∂I⁻(W)` and every pair of Cauchy surfaces `S, S'` with
`S'` nowhere to the past of `S`, the generalized entropy of the exterior `I⁻(W)` does not
decrease: `Sgen (S ∩ I⁻(W)) ≤ Sgen (S' ∩ I⁻(W))`. -/
def FineGrainedGSL (Sgen : Set M → ℝ) : Prop :=
  ∀ (W : ℝ → M) (a : ℝ), st.IsFutureObserver W a →
    ∀ S S' : Set M, st.IsCauchySurface S → st.IsCauchySurface S' →
      S' ⊆ st.causalFuture S →
      Sgen (S ∩ st.chronPast (W '' Ici a)) ≤ Sgen (S' ∩ st.chronPast (W '' Ici a))

/-- The comparison principle of Theorem 1 at the point `g₀`, for the null surface `N` with
exterior `X` (the inner surface) against causal horizons (the outer surface): whenever an
observer `W` has a causal horizon `H = ∂I⁻(W)` such that `N` lies within or on `H`
(`N ∩ I⁻(W) = ∅`) and some future-directed null geodesic segment starting at `g₀` lies on
both `N` and `H`, then decreasing generalized entropy of `X` at `g₀` forces decreasing
generalized entropy of the exterior `I⁻(W)` of `H` at `g₀`.

In the paper this is the content of Theorem 1, derived from the semiclassical
approximation near `g₀`; here it is the formal stand-in for "the semiclassical
approximation is valid near `g₀`". -/
def TheoremOneComparisonAt (Sgen : Set M → ℝ) (N X : Set M) (g₀ : M) : Prop :=
  ∀ (W : ℝ → M) (a : ℝ), st.IsFutureObserver W a →
    N ∩ st.chronPast (W '' Ici a) = ∅ →
    (∃ (γ : ℝ → M) (s b : ℝ), s < b ∧ γ s = g₀ ∧ ContinuousWithinAt γ (Ici s) s ∧
      st.IsGeodesicOn γ (Ioo s b) ∧ (∀ t ∈ Ioo s b, st.IsFutureNull (γ t) (velocity γ t)) ∧
      γ '' Ico s b ⊆ N ∩ frontier (st.chronPast (W '' Ici a))) →
    st.EntropyDecreasingAt Sgen X g₀ →
    st.EntropyDecreasingAt Sgen (st.chronPast (W '' Ici a)) g₀

/-- The null surface `N` shot out from `T` outwards and to the future, where `T` is the
boundary in the Cauchy surface `S` of the exterior region `Ext ⊆ S`: it consists of `T`
together with the part of the boundary of the chronological future of the inner closed
region `S \ Ext` that lies off `S \ Ext`. -/
def outgoingNullSurface (S T Ext : Set M) : Set M :=
  (frontier (st.chronFuture (S \ Ext)) \ (S \ Ext)) ∪ T

/-- The exterior side of the outgoing null surface: the complement of the closure of the
chronological future of the inner region `S \ Ext`. -/
def outgoingExterior (S Ext : Set M) : Set M :=
  (closure (st.chronFuture (S \ Ext)))ᶜ

/-- A quantum trapped surface (§3.2 of the paper).  `S` is a connected Cauchy surface,
`Ext ⊆ S` is a relatively open subset of `S` whose closure is noncompact (the exterior of
`T` on `S` is noncompact), and `T` is its relative boundary in `S`, assumed nonempty and
compact.  Finally, for every point `g₀ ∈ T` the fine-grained generalized entropy of the
exterior of the outgoing null surface shot out from `T` is decreasing at `g₀`, in the
sense of Theorem 3. -/
structure IsQuantumTrappedSurface (Sgen : Set M → ℝ) (S T Ext : Set M) : Prop where
  cauchy : st.IsCauchySurface S
  connected : IsConnected S
  ext_subset : Ext ⊆ S
  ext_relOpen : ∃ V : Set M, IsOpen V ∧ Ext = V ∩ S
  ext_noncompact : ¬ IsCompact (closure Ext)
  boundary_eq : T = (closure Ext ∩ S) \ Ext
  nonempty : T.Nonempty
  compact : IsCompact T
  decreasing : ∀ g₀ ∈ T, st.EntropyDecreasingAt Sgen (st.outgoingExterior S Ext) g₀

end LorentzianMetric

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, §2.2 eq. (10) (GSL, p. 6), Theorem 1 (p. 9), Theorem 3 eq. (33) (p. 14), quantum trapped surface definition (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.

Throughout, $(g,\tau)$ is a LorentzianMetric on $M$ (from WallGSL_Spacetime), $S_{\rm gen}$ is an arbitrary function from subsets of $M$ to $\mathbb R$ (no property of it is assumed in this file), and all sets are arbitrary subsets of $M$ .

Forward deformation of $S$ to $S'$ within $U$ : $S'$ is a Cauchy surface, $S'\setminus U=S\setminus U$ , and $S'\subseteq J^+(S)$ . ( $S$ itself is not required to be Cauchy here.)
Entropy decreasing at $g_0$ for the region $X$ : there exists a Cauchy surface $S$ with $g_0\in S$ such that for every neighbourhood $U$ of $g_0$ there exists $S'$ , a forward deformation of $S$ within $U$ , with

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

Observer from $a$ : $W$ is a future-infinite timelike worldline from $a$ , or a future-infinite null ray from $a$ (definitions in WallGSL_Spacetime).
Fine-grained GSL: for every observer $W$ from $a$ , writing $R=I^-(W([a,\infty)))$ , and every pair of Cauchy surfaces $S,S'$ with $S'\subseteq J^+(S)$ : $S_{\rm gen}(S\cap R)\le S_{\rm gen}(S'\cap R)$ .
Theorem-1 comparison at $g_0$ for $(N,X)$ : for every observer $W$ from $a$ , with $R=I^-(W([a,\infty)))$ : if $N\cap R=\emptyset$ , and there exist $\gamma$ and $s<b$ with $\gamma(s)=g_0$ , $\gamma$ right-continuous at $s$ , $\gamma$ a geodesic on $(s,b)$ with future-null velocity at every $t\in(s,b)$ , and $\gamma([s,b))\subseteq N\cap\partial R$ (topological frontier), and if the entropy is decreasing at $g_0$ for $X$ , then the entropy is decreasing at $g_0$ for $R$ .
Outgoing null surface of $(S,T,\mathrm{Ext})$ : $\big(\partial I^+(S\setminus\mathrm{Ext})\setminus(S\setminus\mathrm{Ext})\big)\cup T$ , where $\partial$ is the topological frontier in $M$ . Outgoing exterior of $(S,\mathrm{Ext})$ : the complement of the closure of $I^+(S\setminus\mathrm{Ext})$ .
Quantum trapped surface $(S_{\rm gen},S,T,\mathrm{Ext})$ — all of: $S$ is a Cauchy surface; $S$ is connected (in particular nonempty); $\mathrm{Ext}\subseteq S$ ; $\mathrm{Ext}=V\cap S$ for some open $V\subseteq M$ ; the closure of $\mathrm{Ext}$ in $M$ is not compact; $T=(\overline{\mathrm{Ext}}\cap S)\setminus\mathrm{Ext}$ ; $T$ is nonempty; $T$ is compact; and for every $g_0\in T$ the entropy is decreasing at $g_0$ for the outgoing exterior of $(S,\mathrm{Ext})$ .

No codimension-2 or smoothness condition is imposed on $T$ , and no condition relates the null surface $N$ to the exterior region $X$ in the comparison predicate other than those listed.

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