Time-oriented Lorentzian spacetimes and causal structure

Definition

WallGSL_Spacetime

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

causalitygeneral-relativitylorentzian-geometry

This definition file sets up time-oriented Lorentzian spacetimes and their causal structure, following §3.2 of Wall (2013) and the standard conventions of Hawking–Ellis.

A Lorentzian metric LorentzianMetric E M on a manifold $M$ modelled on a finite-dimensional real inner product space $E$ consists of

a field of symmetric bilinear forms $g_x$ on the tangent spaces $T_xM\cong E$ , whose components are $C^\infty$ in every chart;
a continuous vector field $\tau$ (timeField) with $g_x(\tau_x,\tau_x)<0$ , such that $g_x$ is positive definite on the $g_x$ -orthogonal complement of $\tau_x$ ; this says that $g_x$ has signature $(-,+,\dots,+)$ , and $\tau$ fixes the time orientation.

On top of this the file defines: future-directed timelike / causal / null vectors; affinely parametrized geodesics through the coordinate geodesic equation $\ddot c^k+\Gamma^k_{ij}\dot c^i\dot c^j=0$ ; $C^1$ future-directed causal and timelike curves; the relations $p\le q$ and $p\ll q$ (finite concatenations of such curves); the sets $I^\pm(S)$ , $J^\pm(S)$ ; achronal sets; global hyperbolicity (no closed timelike curves and $J^+(p)\cap J^-(q)$ compact); inextendible timelike curves; Cauchy surfaces (met exactly once by every inextendible timelike curve); null geodesic completeness (every null geodesic on an open interval extends to a geodesic on all of $\mathbb R$ ); proper time; future-infinite timelike worldlines (timelike, infinite proper time to the future); and future-infinite null rays (future-directed null geodesics defined for all affine parameters $t>a$ ).

These are the geometric notions in which the GSL, quantum trapped surfaces and the singularity theorem are stated.

Formalization Note Tangent spaces are identified with the model space $E$ , as in Mathlib's manifold library. The global hyperbolicity definition is the one written in the paper (footnote 11 there explains why strong causality is not needed).

Definition code

import Mathlib

/-!
# Lorentzian spacetimes and their causal structure

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

A spacetime is a smooth manifold (modelled on a finite-dimensional real inner product
space `E`, without boundary) carrying a smooth Lorentzian metric of signature
`(-,+,…,+)` and a continuous timelike vector field fixing the time orientation.
-/

open scoped Manifold Topology ContDiff
open Set Filter

namespace WallGSL

/-- A time-oriented Lorentzian metric on the manifold `M`.

* `g x` is the metric on the tangent space at `x`, a bilinear form;
* `timeField` is a continuous vector field which is timelike everywhere; it fixes the
  time orientation (a causal vector is future-directed when it has negative `g`-product
  with `timeField`);
* `posDef_orth` says that `g x` is positive definite on the `g x`-orthogonal complement
  of the timelike vector `timeField x`.  Together with `timelike` this says exactly that
  `g x` is nondegenerate of signature `(-,+,…,+)`;
* `smooth` says that in every chart the coordinate components of the metric are `C^∞`. -/
structure LorentzianMetric (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (M : Type*) [TopologicalSpace M] [ChartedSpace E M]
    [IsManifold 𝓘(ℝ, E) ∞ M] where
  /-- The metric tensor. -/
  g : M → E →L[ℝ] E →L[ℝ] ℝ
  /-- A time-orientation vector field. -/
  timeField : M → E
  symm : ∀ x v w, g x v w = g x w v
  timelike : ∀ x, g x (timeField x) (timeField x) < 0
  posDef_orth : ∀ x v, g x v (timeField x) = 0 → v ≠ 0 → 0 < g x v v
  continuous_timeField :
    Continuous (fun x => (⟨x, timeField x⟩ : TangentBundle 𝓘(ℝ, E) M))
  smooth : ∀ p : M, ContDiffOn ℝ ∞
    (fun y : E => (g ((extChartAt 𝓘(ℝ, E) p).symm y)).bilinearComp
      (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) (extChartAt 𝓘(ℝ, E) p).symm y : E →L[ℝ] E)
      (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) (extChartAt 𝓘(ℝ, E) p).symm y : E →L[ℝ] E))
    (extChartAt 𝓘(ℝ, E) p).target

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)

/-- The coordinate expression `G_p(y)` of the metric in the chart at `p`, as a bilinear
form on the model space `E`. -/
noncomputable def coordMetric (p : M) (y : E) : E →L[ℝ] E →L[ℝ] ℝ :=
  (st.g ((extChartAt 𝓘(ℝ, E) p).symm y)).bilinearComp
    (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) (extChartAt 𝓘(ℝ, E) p).symm y : E →L[ℝ] E)
    (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) (extChartAt 𝓘(ℝ, E) p).symm y : E →L[ℝ] E)

/-- The velocity `γ'(t) ∈ T_{γ(t)} M` of a curve `γ : ℝ → M`. -/
noncomputable def velocity (γ : ℝ → M) (t : ℝ) : E :=
  (mfderiv 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ t : ℝ →L[ℝ] E) 1

/-- The one-sided velocity of `γ` at `t`, computed within the set `s`. -/
noncomputable def velocityWithin (γ : ℝ → M) (s : Set ℝ) (t : ℝ) : E :=
  (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ s t : ℝ →L[ℝ] E) 1

/-- A tangent vector is causal and future-directed. -/
def IsFutureCausal (x : M) (v : E) : Prop :=
  st.g x v v ≤ 0 ∧ v ≠ 0 ∧ st.g x v (st.timeField x) < 0

/-- A tangent vector is timelike and future-directed. -/
def IsFutureTimelike (x : M) (v : E) : Prop :=
  st.g x v v < 0 ∧ st.g x v (st.timeField x) < 0

/-- A tangent vector is null (lightlike) and future-directed. -/
def IsFutureNull (x : M) (v : E) : Prop :=
  st.g x v v = 0 ∧ v ≠ 0 ∧ st.g x v (st.timeField x) < 0

/-- `γ` is an affinely parametrized geodesic on the set `s ⊆ ℝ` (intended to be open):
it is `C²` there and, for every `t₀ ∈ s`, the coordinate curve `c = φ ∘ γ` in the chart
`φ` at `γ t₀` satisfies the geodesic equation `c'' + Γ(c)(c', c') = 0` at `t₀`.  The
equation is written with the index lowered, i.e. for every `w ∈ E`
`G(c)(c'', w) + DG(c)[c'](c', w) - ½ DG(c)[w](c', c') = 0`,
which is equivalent to the usual form because `G(c)` is nondegenerate. -/
def IsGeodesicOn (γ : ℝ → M) (s : Set ℝ) : Prop :=
  ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 2 γ s ∧
  ∀ t₀ ∈ s,
    let c : ℝ → E := fun t => extChartAt 𝓘(ℝ, E) (γ t₀) (γ t)
    let G := st.coordMetric (γ t₀)
    ∀ w : E,
      G (c t₀) (deriv (deriv c) t₀) w
        + fderiv ℝ G (c t₀) (deriv c t₀) (deriv c t₀) w
        - (1 / 2 : ℝ) * fderiv ℝ G (c t₀) w (deriv c t₀) (deriv c t₀) = 0

/-- `γ` restricted to `[a, b]` is a `C¹` future-directed causal curve. -/
def IsFutureCausalCurveOn (γ : ℝ → M) (a b : ℝ) : Prop :=
  ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ (Icc a b) ∧
  ∀ t ∈ Icc a b, st.IsFutureCausal (γ t) (velocityWithin γ (Icc a b) t)

/-- `γ` restricted to `[a, b]` is a `C¹` future-directed timelike curve. -/
def IsFutureTimelikeCurveOn (γ : ℝ → M) (a b : ℝ) : Prop :=
  ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ (Icc a b) ∧
  ∀ t ∈ Icc a b, st.IsFutureTimelike (γ t) (velocityWithin γ (Icc a b) t)

/-- One `C¹` future-directed causal segment from `p` to `q`. -/
def CausalStep (p q : M) : Prop :=
  ∃ (γ : ℝ → M) (a b : ℝ), a < b ∧ γ a = p ∧ γ b = q ∧ st.IsFutureCausalCurveOn γ a b

/-- One `C¹` future-directed timelike segment from `p` to `q`. -/
def TimelikeStep (p q : M) : Prop :=
  ∃ (γ : ℝ → M) (a b : ℝ), a < b ∧ γ a = p ∧ γ b = q ∧ st.IsFutureTimelikeCurveOn γ a b

/-- The causal relation `p ≤ q`: `q = p` or `q` is reached from `p` by a piecewise `C¹`
future-directed causal curve. -/
def CausalPrec (p q : M) : Prop := Relation.ReflTransGen st.CausalStep p q

/-- The chronological relation `p ≪ q`: `q` is reached from `p` by a piecewise `C¹`
future-directed timelike curve. -/
def ChronPrec (p q : M) : Prop := Relation.TransGen st.TimelikeStep p q

/-- Chronological future `I⁺(S)`. -/
def chronFuture (S : Set M) : Set M := {q | ∃ p ∈ S, st.ChronPrec p q}

/-- Chronological past `I⁻(S)`. -/
def chronPast (S : Set M) : Set M := {q | ∃ p ∈ S, st.ChronPrec q p}

/-- Causal future `J⁺(S)`. -/
def causalFuture (S : Set M) : Set M := {q | ∃ p ∈ S, st.CausalPrec p q}

/-- Causal past `J⁻(S)`. -/
def causalPast (S : Set M) : Set M := {q | ∃ p ∈ S, st.CausalPrec q p}

/-- A set is achronal: no two of its points are chronologically related. -/
def IsAchronal (S : Set M) : Prop := ∀ p ∈ S, ∀ q ∈ S, ¬ st.ChronPrec p q

/-- Global hyperbolicity in the sense of the paper (§3.2): there are no closed timelike
curves, and `J⁺(p) ∩ J⁻(q)` is compact for all points `p, q`. -/
def IsGloballyHyperbolic : Prop :=
  (∀ p : M, ¬ st.ChronPrec p p) ∧
  ∀ p q : M, IsCompact (st.causalFuture {p} ∩ st.causalPast {q})

/-- An inextendible timelike curve, parametrized by all of `ℝ`: it is future-directed
timelike on every compact parameter interval and has no endpoint in either direction. -/
def IsInextendibleTimelike (γ : ℝ → M) : Prop :=
  (∀ a b, a < b → st.IsFutureTimelikeCurveOn γ a b) ∧
  (¬ ∃ x, Tendsto γ atTop (𝓝 x)) ∧ (¬ ∃ x, Tendsto γ atBot (𝓝 x))

/-- A Cauchy surface: a set met exactly once by every inextendible timelike curve. -/
def IsCauchySurface (S : Set M) : Prop :=
  ∀ γ : ℝ → M, st.IsInextendibleTimelike γ → ∃! t, γ t ∈ S

/-- Null geodesic completeness: every null geodesic defined on an open interval extends
to a geodesic defined on all of `ℝ` (i.e. it can be continued to all values of its
affine parameter). -/
def IsNullGeodesicallyComplete : Prop :=
  ∀ (γ : ℝ → M) (a b : ℝ), a < b → st.IsGeodesicOn γ (Ioo a b) →
    (∀ t ∈ Ioo a b, st.g (γ t) (velocity γ t) (velocity γ t) = 0 ∧ velocity (E := E) γ t ≠ 0) →
    ∃ δ : ℝ → M, st.IsGeodesicOn δ univ ∧ EqOn δ γ (Ioo a b)

/-- The proper time `∫ₐᵇ √(-g(γ', γ')) dt` of a curve between parameters `a` and `b`. -/
noncomputable def properTime (γ : ℝ → M) (a b : ℝ) : ℝ :=
  ∫ t in a..b, Real.sqrt (-(st.g (γ t) (velocity γ t) (velocity γ t)))

/-- A future-infinite timelike worldline (an "observer") starting at parameter `a`:
future-directed timelike on every `[a, b]`, with infinite proper time to the future. -/
def IsFutureInfiniteTimelike (W : ℝ → M) (a : ℝ) : Prop :=
  (∀ b, a < b → st.IsFutureTimelikeCurveOn W a b) ∧
  Tendsto (fun b => st.properTime W a b) atTop atTop

/-- A future-directed null geodesic ray starting at `W a` whose affine parameter is
infinite to the future: `W` is a geodesic on `(a, ∞)`, continuous from the right at `a`,
with future-directed null velocity. -/
def IsFutureInfiniteNullRay (W : ℝ → M) (a : ℝ) : Prop :=
  st.IsGeodesicOn W (Ioi a) ∧ ContinuousWithinAt W (Ici a) a ∧
  ∀ t > a, st.IsFutureNull (W t) (velocity W t)

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, §3.2 (global hyperbolicity, p. 15), §2.2 (observers, p. 6)

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.

This file declares, for a manifold $M$ with charts into a finite-dimensional real inner product space $E$ and a $C^\infty$ manifold structure (no Hausdorff or second-countability assumption is made in this file), the following.

The structure LorentzianMetric E M. Data: a function $g$ assigning to each $x\in M$ a continuous bilinear form $g_x:E\times E\to\mathbb R$ , and a function $\tau:M\to E$ . Conditions:

$g_x(v,w)=g_x(w,v)$ for all $x,v,w$ ;
$g_x(\tau_x,\tau_x)<0$ for all $x$ ;
for all $x$ and $v\neq 0$ with $g_x(v,\tau_x)=0$ : $g_x(v,v)>0$ ;
the map $x\mapsto(x,\tau_x)$ into the tangent bundle is continuous;
for every $p\in M$ , writing $\varphi_p$ for the extended chart at $p$ , the map $y\mapsto G_p(y)$ , $G_p(y)(u,w)=g_{\varphi_p^{-1}(y)}\big(D\varphi_p^{-1}(y)u,\ D\varphi_p^{-1}(y)w\big)$ , is $C^\infty$ on the chart's target. ( $D\varphi_p^{-1}$ is Mathlib's manifold derivative, which takes the value $0$ wherever $\varphi_p^{-1}$ is not differentiable.)

Vectors. At $x$ , $v\in E$ is future causal iff $g_x(v,v)\le 0$ , $v\ne0$ , $g_x(v,\tau_x)<0$ ; future timelike iff $g_x(v,v)<0$ and $g_x(v,\tau_x)<0$ ; future null iff $g_x(v,v)=0$ , $v\ne 0$ , $g_x(v,\tau_x)<0$ .

Velocity. For $\gamma:\mathbb R\to M$ , $\dot\gamma(t)$ is the manifold derivative applied to $1$ (zero where not differentiable); the within- $s$ version uses the derivative within the set $s$ .

Geodesic on a set $s\subseteq\mathbb R$ (IsGeodesicOn): $\gamma$ is $C^2$ on $s$ , and for every $t_0\in s$ , with $c(t)=\varphi_{\gamma(t_0)}(\gamma(t))$ and $G=G_{\gamma(t_0)}$ , for every $w\in E$ :

G(c(t_0))(\ddot c(t_0),w)+DG(c(t_0))[\dot c(t_0)](\dot c(t_0),w)-\tfrac12\,DG(c(t_0))[w](\dot c(t_0),\dot c(t_0))=0,

where $\dot c,\ddot c$ are ordinary derivatives (zero where they do not exist) and $DG$ is the Fréchet derivative. The set $s$ is not required to be open.

Curves on $[a,b]$ . Future causal (resp. timelike) curve on $[a,b]$ : $C^1$ on $[a,b]$ and the within- $[a,b]$ velocity is future causal (resp. future timelike) at every $t\in[a,b]$ . No condition $a<b$ is built in.

Relations. A causal (timelike) step $p\to q$ : some $\gamma$ and $a<b$ with $\gamma(a)=p$ , $\gamma(b)=q$ , $\gamma$ future causal (timelike) on $[a,b]$ . $p\le q$ is the reflexive–transitive closure of causal steps (so $p\le p$ always); $p\ll q$ is the transitive closure of timelike steps. $I^+(S)=\{q:\exists p\in S,\ p\ll q\}$ , $I^-(S)=\{q:\exists p\in S,\ q\ll p\}$ , and $J^\pm(S)$ likewise with $\le$ . $S$ is achronal iff no $p,q\in S$ satisfy $p\ll q$ (this includes $p=q$ ).

Global hyperbolicity: $\neg(p\ll p)$ for all $p$ , and $J^+(\{p\})\cap J^-(\{q\})$ is compact for all $p,q$ .

Inextendible timelike curve $\gamma:\mathbb R\to M$ : future timelike on every $[a,b]$ with $a<b$ , and $\gamma(t)$ has no limit as $t\to+\infty$ and none as $t\to-\infty$ .

Cauchy surface $S$ : every inextendible timelike curve $\gamma$ has exactly one parameter $t$ with $\gamma(t)\in S$ . (No achronality, closedness or regularity of $S$ is required beyond this.)

Null geodesic completeness: for every $\gamma$ and $a<b$ such that $\gamma$ is a geodesic on $(a,b)$ and $g(\dot\gamma(t),\dot\gamma(t))=0$ , $\dot\gamma(t)\ne0$ for all $t\in(a,b)$ (no future-direction requirement), there is $\delta$ which is a geodesic on all of $\mathbb R$ and agrees with $\gamma$ on $(a,b)$ .

Proper time from $a$ to $b$ : $\int_a^b\sqrt{-g(\dot\gamma,\dot\gamma)}\,dt$ (interval integral; $\sqrt{\cdot}$ of a negative number is $0$ , and a non-integrable integrand gives the value $0$ ).

Future-infinite timelike worldline from $a$ : future timelike on $[a,b]$ for every $b>a$ , and the proper time from $a$ to $b$ tends to $+\infty$ as $b\to\infty$ .

Future-infinite null ray from $a$ : $W$ is a geodesic on $(a,\infty)$ , continuous at $a$ from the right, and $\dot W(t)$ is future null for every $t>a$ .

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