This chapter describes how the library encodes spacetimes, their causal structure, the regions to
which the Haag–Kastler axioms attach algebras, the symmetries that act on them, and the geometry
underneath: the Levi-Civita connection and geodesics. It corresponds to Section 10.5 of the
blueprint.
The physics is introduced in chapter 1 of the tutorial, and the Lean
needed to read the declarations in chapter 2; this chapter assumes
both.
5.2. Design🔗
The conventions of the causal structure are stated once in the conventions chapter, under
Causal structure.
The blueprint is the specification, and its entries record the reasons for the choices below. The
reasons for the regions and topology of Minkowski space are set out at length in the blueprint's
chapter 2,
which is context and is not formalised.
5.2.1. A spacetime is a structure🔗
Mathlib has Riemannian metrics but no Lorentzian or pseudo-Riemannian ones, so Spacetime is
built from Mathlib's primitives: a structure bundling the carrier type, its topology and atlas as
instance fields, and the metric val with its conditions. Two details of the encoding matter when
reading the Lean.
-
Smoothness is a bundle condition. The field contMDiff has the shape of the smoothness field
of Mathlib's Bundle.ContMDiffRiemannianMetric, so Mathlib's bundle API applies; the Riemannian
class itself is not used, since its positivity fields fail for a Lorentzian form.
-
The time orientation is separate data. It is an argument of every causal notion, as in
ChronologicallyPrecedes M t p q, written p ≪[M, t] q.
The blueprint entry def:spacetime
records the reasons for the smoothness clause and the regularity index; the
conventions chapter explains the index.
5.2.2. Minkowski space and the Alexandrov topology🔗
As you will recall from chapter 1 of the tutorial,
the 1964 axioms attach algebras to open sets without naming the topology, and the project uses the
Alexandrov topology, generated by the diamonds I^+(p) \cap I^-(q). It is defined from the light
cones alone, and on Minkowski space it coincides with the Euclidean topology.
The library has two Minkowski spacetimes, which differ only in the topology instance on the
carrier: StandardMinkowskiSpacetime, with the Euclidean topology, on which all the Minkowski
results are stated, and MinkowskiSpacetime, the blueprint's Minkowski spacetime, with the
Alexandrov topology. They are interchangeable because the two topologies coincide
(alexandrov_eq_euclidean_standardMinkowski). Spacetime.alexandrovTopology M t is a reducible
definition, not an instance, so that it never competes with the manifold topology on the same
type; a statement about it names it explicitly, as @IsOpen M.Carrier (alexandrovTopology M t).
5.2.3. Paths and curves🔗
Two design points of the definitions matter. A smooth path has a velocity \dot\mu(s) that
vanishes nowhere, endpoints included; this excludes constant paths, so a null path moves along the
light cone instead of resting at a point. And past and future endpoints are defined by extremality
of the parameter, not by the boundary of the parameter interval \Sigma, so they make sense for
every parameter space, including [0, \infty) and \mathbb{R} (blueprint
def:endpoints).
5.2.4. Causal precedence is defined by curves🔗
On Minkowski space p \prec q could be defined by vectors: q - p is causal and
future-directed, or zero. The library defines it by curves, as the blueprint does, so that one
definition serves every spacetime: p \ll q and IsCausalTrip t p q are chains of one or more
timelike or causal geodesic segments, and p \prec q is a chain of zero or more causal segments.
So \prec is reflexive, p \prec p for every p, while IsCausalTrip is strict;
causallyPrecedes_iff_eq_or_isCausalTrip connects the two. Two consequences are worth knowing. No
point is spacelike to itself, so a region and its spacelike complement are disjoint. And the
causality condition NoClosedCausalCurve is stated with the strict relation, as "no causal trip
from p to p"; stated as \lnot(p \prec p) it would fail in every spacetime. The reasons
for the reflexive convention are in the conventions chapter (blueprint
def:causal-trip).
The closure operators Relation.TransGen and Relation.ReflTransGen are what make transitivity
free: concatenating two chains is a chain, so causallyPrecedes_trans is
Relation.ReflTransGen.trans.
The Alexandrov topology is TopologicalSpace.generateFrom of the family alexandrovBasis M t of
chronological diamonds, so the diamonds are a subbasis by construction, and every diamond is open.
That they form a basis is a theorem with hypotheses; it needs three conditions:
-
the diamonds generate the topology, which holds by definition;
-
they cover the space; on a LorentzianSpacetime with at least two points this follows from the
Hausdorff condition, since a point in no diamond would have the whole space as its only open
neighbourhood;
-
they have the intersection property: every point in the intersection of two diamonds lies in a
diamond inside that intersection. In the standard theory it holds in every spacetime, since
chronological futures are open in the manifold topology; this is not proved in the library, so
LorentzianSpacetime.isTopologicalBasis_alexandrovBasis takes it as the hypothesis hdir. On
standard Minkowski space it is proved, and the diamonds form a basis unconditionally.
The intersection property should not be confused with upward directedness, that any two diamonds
lie in a common diamond (alexandrovBasis_directed). The first makes the diamonds a basis; the
second makes the local algebras of a net a directed system, and it is what the quasilocal
algebra and the Minkowski form of Axiom 3 use (blueprint
lmm:minkowski-diamonds-upward-directed).
In a curved spacetime two diamonds need not lie in a common diamond, which is why the
Haag–Kastler chapter states
Axiom 3 in a common diamond.
A diamond can be empty: I^+(p) \cap I^-(q) is empty unless p \ll q, so on Minkowski space
the empty set is a diamond. The causal diamonds J^+(p) \cap J^-(q) are also defined, with their
structure lemmas, but on Minkowski space they are closed, and they are not the regions of the
net; the
tutorial
explains why.
5.2.6. Causal complements🔗
The spacelike complement \mathbf{B}^\perp of a region is the set of points spacelike to every
point of \mathbf{B}. It is the geometric side of locality: by Einstein causality, observables
in \mathbf{B}^\perp commute with those in \mathbf{B}. Complementation is the Galois
connection of the relation "spacelike related", so the causal closure
\mathbf{B} \mapsto \mathbf{B}^{\perp\perp} is a closure operator, and the causally complete
regions, \mathbf{B}^{\perp\perp} = \mathbf{B}, form a complete lattice.
Because no point is spacelike to itself, the causal complement is an orthocomplement on this
lattice. Causally complete regions are a common index set for local algebras in the literature;
the library's Haag–Kastler net is indexed by diamonds instead.
5.2.7. Symmetries🔗
For Minkowski space the symmetries form the inhomogeneous Lorentz group; tutorial
chapter 3 proves that they preserve
causal precedence.
For a general spacetime the symmetries are the isometries. The curved-spacetime Axiom 5 asks for
the isometries "connected to the identity", and these must map diamonds to diamonds. An isometry
preserves the causal type of vectors, but it may reverse the time orientation, and then it can map
I^+(p) onto I^-(\varphi(p)). The library therefore uses orientedIdentityComponent: the
isometries in the identity component that, with their inverses, preserve the future orientation.
This is an implementation choice, not a restriction: the oriented identity component is the whole
identity component, but the proof needs a Myers–Steenrod-type rigidity theorem, which Mathlib does
not provide, so the library puts orientation preservation into the definition (blueprint
def:isometric-covariance-in-curved-spacetime,
formalization note). The conventions chapter discusses it
further.
Preserving the causal structure is weaker than being an isometry: a dilation
x \mapsto \lambda x, \lambda > 0, maps diamonds to diamonds but scales \eta by
\lambda^2 (alexandrovBasis_image_smul, exists_minkowskiForm_smul_ne). Covariance is
therefore stated for isometries, not for a metric-free notion of causal automorphism.
5.2.8. The pseudo-Riemannian layer🔗
Trips are built from geodesics, and Mathlib has neither geodesics nor a Levi-Civita connection for
an indefinite metric. The library supplies them in Physicslib4/Geometry/PseudoRiemannian/, for
any finite-dimensional smooth manifold and any signature; a spacetime metric enters through
Spacetime.toPseudoRiemannianMetric, and the Lorentzian signature is never used in this layer.
The construction follows Mathlib's Riemannian one with the inner product replaced by g. A
covariant derivative is Mathlib's CovariantDerivative; IsLeviCivitaFor g ∇ says it is
torsion-free and metric compatible. The right-hand side of the Koszul formula is tensorial in
X and Z, so for each Y it defines at every point a bilinear form in X(x) and Z(x),
and the musical isomorphism v \mapsto g_x(v, \cdot), invertible by non-degeneracy, turns it into
\nabla_X Y. No chart appears in any definition; charts and local frames are used only inside
proofs.
A geodesic is defined chart-free, as \nabla_{\dot\mu}\dot\mu = 0 tested against smooth
extensions of the velocity, so it is affinely parametrised. The condition is imposed at interior
parameters only; at an endpoint it would follow by continuity, which the library does not prove
(blueprint
def:geodesic).
5.3. Main definitions and theorems🔗
Definitions are shown with their docstrings, which give the mathematics and the blueprint entry;
theorems with their statements, as Lean prints them, and a line or two of explanation. Each
subsection opens with the blueprint entries it covers. In the printed statements, M.Carrier is
the set of points of the spacetime M, p ≺[M, t] q is causal precedence for the time orientation
t, and M.IsCausalTrip t p q is Lean's dot notation for Spacetime.IsCausalTrip M t p q. For
the declarations not shown here, see the
API documentation
and the files listed at the end of the chapter.
5.3.1. Spacetimes and time orientations🔗
Blueprint: def:spacetime, def:timelike-spacelike-null-vectors,
def:time-orientable, def:future-and-past-pointing-vectors.
The structure, with its fields. The manifold structure is in the bracketed fields (topology,
chartedSpace, isManifold and the like), which the library registers as instances, so that Lean
finds them wherever M : Spacetime is in scope:
🔗structure
A spacetime: a connected four-dimensional smooth manifold with a Lorentzian metric.
A spacetime is a real, four-dimensional, connected, smooth, Hausdorff manifold M without
boundary, together with a smooth symmetric tensor field g of type (0, 2) that is non-degenerate
and Lorentzian: at every point x there is a basis of the tangent space TₓM in which g_x is
diag(-1, 1, 1, 1). This is the signature convention (-, +, +, +), so a tangent vector v is
timelike when g_x(v, v) < 0 (Spacetime.IsTimelike).
The structure carries no time orientation and no topology other than the manifold topology;
these are separate data (Spacetime.TimeOrientation, Spacetime.alexandrovTopology,
Spacetime.LorentzianSpacetime).
Implementation note: Mathlib has no Lorentzian metric type, so the manifold and its metric are
unbundled into Mathlib primitives. The manifold is the type Carrier with instance fields for
the topology, the Hausdorff and connectedness conditions, the charts modelled on
SpacetimeModel (ℝ⁴) and C^∞ smoothness. The metric is the family val of continuous
bilinear forms on the tangent spaces, with the conditions symm, nondegenerate, lorentzian
and contMDiff. Smoothness is stated as smoothness of a section of the bundle of bilinear forms
on the tangent bundle, the same shape as Bundle.ContMDiffRiemannianMetric.contMDiff, so
Mathlib's bundle API (ContMDiff.clm_bundle_apply₂) gives smoothness of x ↦ g_x(V(x), W(x))
for smooth vector fields V and W. The general pseudo-Riemannian API is reached through
Spacetime.toPseudoRiemannianMetric.
Blueprint: def:spacetime
Fields
Carrier : Type u_1
The points of the spacetime manifold M.
topology : TopologicalSpace self.Carrier
The manifold topology of M.
connected : ConnectedSpace self.Carrier
chartedSpace : ChartedSpace SpacetimeModel self.Carrier
The atlas of M, with charts valued in the model space ℝ⁴ (SpacetimeModel).
model : ModelWithCorners ℝ SpacetimeModel SpacetimeModel
The model with corners of the smooth structure on M.
It is usually modelWithCornersSelf ℝ SpacetimeModel; the field boundaryless requires
only that it has no boundary.
isManifold : IsManifold self.model (↑⊤) self.Carrier
M is a C^∞ manifold modelled on ℝ⁴.
Implementation note: the field is instance-implicit because the field contMDiff needs the
tangent bundle's FiberBundle and VectorBundle instances, which require IsManifold.
boundaryless : self.model.Boundaryless
M has no boundary: chart targets are open in ℝ⁴.
The pseudo-Riemannian layer (the Levi-Civita connection and geodesics) uses open chart
targets.
tangent_findim : ∀ (x : self.Carrier), FiniteDimensional ℝ (TangentSpace self.model x)
Each tangent space TₓM is finite-dimensional.
val : (x : self.Carrier) → TangentSpace self.model x →L[ℝ] TangentSpace self.model x →L[ℝ] ℝ
The metric g: at each point x, a continuous bilinear form g_x on the tangent space TₓM.
symm : ∀ (x : self.Carrier) (v w : TangentSpace self.model x), ((self.val x) v) w = ((self.val x) w) v
g is symmetric: g_x(v, w) = g_x(w, v).
nondegenerate : ∀ (x : self.Carrier) (v : TangentSpace self.model x),
(∀ (w : TangentSpace self.model x), ((self.val x) v) w = 0) → v = 0
g is non-degenerate: if g_x(v, w) = 0 for every w, then v = 0.
lorentzian : ∀ (x : self.Carrier), LorentzianAt fun v w => ((self.val x) v) w
g is Lorentzian: at every point x some basis of TₓM has Gram matrix diag(-1, 1, 1, 1)
(LorentzianAt).
contMDiff : ContMDiff self.model (self.model.prod (modelWithCornersSelf ℝ (SpacetimeModel →L[ℝ] SpacetimeModel →L[ℝ] ℝ))) ↑⊤
fun x => ⟨x, self.val x⟩
g is smooth: it is a C^∞ section of the bundle of continuous bilinear forms on the
tangent bundle, whose fibre at x is the space of bilinear forms on TₓM.
Implementation note: the statement has the shape of
Bundle.ContMDiffRiemannianMetric.contMDiff, so that Mathlib's bundle API applies; in
particular ContMDiff.clm_bundle_apply₂ gives smoothness of x ↦ g_x(V(x), W(x)) for smooth
vector fields V and W, which causal and geodesic arguments need. Only the shape is reused,
not the class: ContMDiffRiemannianMetric also carries pos and isVonNBounded, and the
latter is false for a Lorentzian form, since {v | g(v, v) < 1} contains the whole light cone.
A chart-local ContDiffWithinAt formulation would give no route to the bundle API, since
Mathlib has no lemma relating the two forms.
The causal type of a tangent vector is the sign of g_x(v, v): Spacetime.IsTimelike,
Spacetime.IsNull and Spacetime.IsSpacelike, exactly one of which holds
(isTimelike_or_isNull_or_isSpacelike). A time orientation picks the future half of each cone:
🔗structure
A time orientation of a spacetime: a smooth, nowhere-vanishing, everywhere timelike vector field.
A time orientation t decides at every point which half of the light cone is the future: a
timelike vector v is future-pointing when g_x(t(x), v) < 0 (Spacetime.IsFuturePointing), that
is, when it lies in the same half of the cone as t(x). A spacetime that has a time orientation is
time-orientable (Spacetime.IsTimeOrientable). For standard Minkowski spacetime the usual choice
is the constant field e₀ = ∂₀ (standardMinkowskiTimeOrientation).
The causal relations of the library (≪, ≺, the futures and pasts I⁺(p), J⁺(p), and the
Alexandrov topology) all take a time orientation as an argument.
Blueprint: def:time-orientable
Fields
field : (x : M.Carrier) → TangentSpace M.model x
The vector field t: a tangent vector t(x) at each point x.
nonvanishing : ∀ (x : M.Carrier), self.field x ≠ 0
t vanishes nowhere: t(x) ≠ 0.
timelike_at : ∀ (x : M.Carrier), M.IsTimelike (self.field x)
t is timelike everywhere: g_x(t(x), t(x)) < 0.
smooth : ContMDiff M.model M.model.tangent ↑⊤ fun x => ⟨x, self.field x⟩
t is smooth: it is a C^∞ section of the tangent bundle.
Implementation note: the statement is Mathlib's bundle-section idiom, matching the field
Spacetime.contMDiff of the metric. It is the left-hand side of Bundle.contMDiffAt_section,
the hypothesis of ContMDiff.mpullback_vectorField and an input of
ContMDiff.clm_bundle_apply₂. A chart-local double-mfderiv formulation would need a
hand-built bridge in both directions, since Mathlib relates tangentCoordChange to
neither.
🔗def
A tangent vector is future-pointing for a time orientation t: timelike with
g_x(t(x), v) < 0, or null and a limit of such vectors.
A timelike v is future-pointing when g_x(t(x), v) < 0, so that v and t(x) lie in the same half
of the light cone. A null v is future-pointing when it is the limit of a sequence of
future-pointing timelike vectors, so the future-pointing null vectors form the boundary of the
future timelike cone. The zero vector, the limit of ε t(x) as ε → 0, is both future- and
past-pointing; curves exclude it by requiring a non-vanishing velocity (SmoothPath).
Spacelike vectors are neither future- nor past-pointing.
Blueprint: def:future-and-past-pointing-vectors
The future-pointing vectors at a point form a convex cone, null boundary included
(isFuturePointing_add_general);
the proof runs through the reverse Cauchy–Schwarz inequality for timelike vectors,
g(v,v)\,g(w,w) \le g(v,w)^2, in LorentzCauchySchwarz.lean.
5.3.2. Paths, curves and geodesics🔗
Blueprint: def:paths, def:curves, def:endpoints,
def:geodesic.
🔗structure
A path in a spacetime: a continuous map μ : Σ → M on a closed interval Σ of ℝ with more than one
point.
The parameter space Σ is a closed, connected subset of ℝ with at least two points, that is, a
non-degenerate closed interval, bounded or not: [a, b], [a, ∞), (-∞, b] or ℝ. A path is a
parametrised object; the unparametrised curve is its class under reparametrisation (Curve).
Implementation note: Σ is stored as a Set ℝ with proofs of the three conditions, and μ as a
function on all of ℝ that is continuous on Σ; its values off Σ are never used.
Blueprint: def:paths
Fields
parameterSpace : Set ℝ
The parameter space Σ ⊆ ℝ.
isConnected : IsConnected self.parameterSpace
Σ is connected (so it is an interval) and non-empty.
toFun : ℝ → M.Carrier
The map μ, defined on all of ℝ; only its values on Σ matter.
SmoothPath extends Path; its own fields are smoothness and the non-vanishing velocity:
🔗structure
A smooth path: a path μ : Σ → M that is C^∞ on Σ and whose velocity vanishes nowhere on Σ.
The velocity μ̇(s) is the derivative of μ at s along Σ (SmoothPath.tangent), one-sided at an
endpoint of Σ. Requiring μ̇(s) ≠ 0 everywhere, endpoints included, excludes paths that stop,
such as constant paths, so a smooth path whose velocity is null moves along the light cone.
Blueprint: def:paths
Fields
nonvanishing : ∀ s ∈ self.parameterSpace, (mfderiv[self.parameterSpace] self.toFun s) 1 ≠ 0
The velocity vanishes nowhere: μ̇(s) ≠ 0 for every s ∈ Σ, endpoints included.
The velocity is the derivative of μ within Σ (mfderivWithin) applied to 1 ∈ ℝ.
The velocity \dot\mu(s) is SmoothPath.tangent. The classes under reparametrisation are
Curve, SmoothCurve and OrientedSmoothCurve; the causal type is well defined on smooth curves
(isTimelikeSmoothCurve_ofPath_iff), and the orientation on oriented ones
(isFutureOrientedCurve_ofPath_iff). The geodesic condition:
🔗def
A smooth path is a geodesic: its velocity is parallel along it for the Levi-Civita connection,
∇_(μ̇) μ̇ = 0.
Precisely, for every interior parameter s of Σ and every smooth vector field X on M with
X(μ(t)) = μ̇(t) for t near s, the covariant derivative (∇_X X)(μ(s)) vanishes, where ∇ is the
Levi-Civita connection of the metric (Geometry.PseudoRiemannianMetric.leviCivita). This is
the geodesic equation μ̈ + Γ(μ̇, μ̇) = 0 written without charts or Christoffel symbols.
The condition is on the path, not on its curve: geodesics are affinely parametrised, and a
reparametrisation μ ∘ σ is again a geodesic only when σ is affine.
The value (∇_X X)(μ(s)) depends only on X along μ (SmoothPath.covDeriv_eq_of_eventuallyEq), and
such an X exists near every interior parameter (SmoothPath.exists_vectorField_eq_tangent), so
the condition is neither ambiguous nor vacuous. It is imposed only at interior parameters; at an
endpoint of Σ it would follow by continuity of the velocity, which the library does not state.
Blueprint: def:geodesic
5.3.3. Causal relations🔗
Blueprint: def:trip, def:causal-trip,
thrm:precedence-transitive, def:no-closed-causal-curve,
thrm:causal-order-refinements, def:spacelike-related,
def:completely-spacelike.
The three relations, from the strict ones to the reflexive one. A single segment is
IsTripSegment or IsCausalTripSegment; the relations chain them.
🔗def
Chronological precedence p ≪ q: there is a trip from p to q, for the time orientation t.
In standard Minkowski spacetime p ≪ q exactly when q - p lies in the open future light cone
(chronologicalFuture_standardMinkowski). The relation
is transitive, and irreflexive when there is no closed causal curve
(chronologicallyPrecedes_irrefl). The notation is p ≪[M, t] q.
Blueprint: def:trip
🔗def
There is a causal trip from p to q: a finite chain of one or more causal trip segments.
This relation is strict: it asks for at least one segment, a genuine curve with non-vanishing
velocity, so IsCausalTrip t p p means a closed causal curve through p, which
NoClosedCausalCurve forbids. The reflexive relation is causal precedence ≺
(CausallyPrecedes), and p ≺ q exactly when p = q or there is a causal trip from p to q
(causallyPrecedes_iff_eq_or_isCausalTrip).
Implementation note: the chain is the transitive closure Relation.TransGen of
CausalSegmentPrecedes.
Blueprint: def:causal-trip
🔗def
Causal precedence p ≺ q: p = q, or there is a causal trip from p to q.
The relation is reflexive: p ≺ p holds for every p, by the chain of no segments
(causallyPrecedes_refl). This is the Hawking–Ellis convention p ∈ J⁺(p), in which the trivial
case p = q plays the role of a degenerate causal curve. The strict relation, one or more
segments, is IsCausalTrip (causallyPrecedes_iff_eq_or_isCausalTrip). Causal precedence is
transitive (causallyPrecedes_trans), and it is antisymmetric, hence a partial order, when there
is no closed causal curve (causallyPrecedes_antisymm). Chronological precedence implies it
(causallyPrecedes_of_chronologicallyPrecedes). The notation is p ≺[M, t] q.
Implementation note: the relation is the reflexive-transitive closure Relation.ReflTransGen of
CausalSegmentPrecedes, a chain of zero or more causal trip segments.
Blueprint: def:causal-trip
Reflexivity is the chain of no segments, and transitivity is concatenation of chains:
open Physicslib4 Spacetime in
Physicslib4.Spacetime.causallyPrecedes_refl (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : p ≺[M, t] p#check causallyPrecedes_refl
Physicslib4.Spacetime.causallyPrecedes_refl (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : p ≺[M, t] p
open Physicslib4 Spacetime in
Physicslib4.Spacetime.causallyPrecedes_trans (M : Spacetime) (t : M.TimeOrientation) {p q r : M.Carrier}
(h₁ : p ≺[M, t] q) (h₂ : q ≺[M, t] r) : p ≺[M, t] r#check causallyPrecedes_trans
Physicslib4.Spacetime.causallyPrecedes_trans (M : Spacetime) (t : M.TimeOrientation) {p q r : M.Carrier}
(h₁ : p ≺[M, t] q) (h₂ : q ≺[M, t] r) : p ≺[M, t] r
The reflexive relation is the strict one plus equality. chronologicallyPrecedes_trans and
isCausalTrip_trans are the transitivity of the strict relations, and
causallyPrecedes_of_chronologicallyPrecedes says that p \ll q implies p \prec q.
open Physicslib4 Spacetime in
Physicslib4.Spacetime.causallyPrecedes_iff_eq_or_isCausalTrip (M : Spacetime) (t : M.TimeOrientation)
{p q : M.Carrier} : (p ≺[M, t] q) ↔ p = q ∨ M.IsCausalTrip t p q#check causallyPrecedes_iff_eq_or_isCausalTrip
Physicslib4.Spacetime.causallyPrecedes_iff_eq_or_isCausalTrip (M : Spacetime) (t : M.TimeOrientation)
{p q : M.Carrier} : (p ≺[M, t] q) ↔ p = q ∨ M.IsCausalTrip t p q
The causality condition forbids closed causal curves, stated with the strict relation:
🔗def
The causality condition: no causal trip runs from a point back to itself.
A closed causal curve through p is a causal trip from p to p (IsCausalTrip, one or more
segments), and the condition forbids it for every p. The condition is not ¬(p ≺ p), which fails
in every spacetime because ≺ is reflexive. It is strictly weaker than strong causality and
strictly stronger than the chronology condition ¬(p ≪ p). Under it, ≪ is irreflexive and ≺ is a
partial order (chronologicallyPrecedes_irrefl, causallyPrecedes_antisymm).
Blueprint: def:no-closed-causal-curve
Under it, causal trips are asymmetric, since two opposite trips concatenate to a closed one, and
\prec is antisymmetric, hence a partial order; chronologicallyPrecedes_irrefl gives
\lnot(p \ll p).
open Physicslib4 Spacetime in
Physicslib4.Spacetime.isCausalTrip_asymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t)
{p q : M.Carrier} (hpq : M.IsCausalTrip t p q) : ¬M.IsCausalTrip t q p#check isCausalTrip_asymm
Physicslib4.Spacetime.isCausalTrip_asymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t)
{p q : M.Carrier} (hpq : M.IsCausalTrip t p q) : ¬M.IsCausalTrip t q popen Physicslib4 Spacetime in
Physicslib4.Spacetime.causallyPrecedes_antisymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t)
{p q : M.Carrier} (hpq : p ≺[M, t] q) (hqp : q ≺[M, t] p) : p = q#check causallyPrecedes_antisymm
Physicslib4.Spacetime.causallyPrecedes_antisymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t)
{p q : M.Carrier} (hpq : p ≺[M, t] q) (hqp : q ≺[M, t] p) : p = q
The futures and pasts are the sets chronologicalFuture M t p = I^+(p),
chronologicalPast, causalFuture = J^+(p) and causalPast, with set-valued versions such as
causalFutureSet = J^+(S). Spacelike separation is the absence of causal precedence in both
directions:
🔗def
Two regions are completely spacelike: every point of O₁ is spacelike related to every point
of O₂.
This is the separation under which observables of the two regions commute in the Haag–Kastler
axioms (Einstein causality). The relation is symmetric (isCompletelySpacelike_comm), and
completely spacelike regions are disjoint, since no point is spacelike related to itself.
Blueprint: def:completely-spacelike
Because \prec is reflexive, no point is spacelike to itself:
open Physicslib4 Spacetime in
Physicslib4.Spacetime.isSpacelikeRelated_irrefl (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) :
¬M.IsSpacelikeRelated t p p#check isSpacelikeRelated_irrefl
Physicslib4.Spacetime.isSpacelikeRelated_irrefl (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) :
¬M.IsSpacelikeRelated t p p
5.3.4. Diamonds and the Alexandrov topology🔗
Blueprint: def:causal-diamond, lmm:causal-diamond-structure,
thrm:causal-diamond-vs-chronological, def:causally-convex-region,
def:alexandrov-topology, def:lorentzian-spacetime,
thrm:alexandrov-topological-basis.
The two kinds of diamond. The chronological ones are the regions of the net:
🔗def
The chronological (Alexandrov) diamond I⁺(p) ∩ I⁻(q) of two points: the points x with p ≪ x
and x ≪ q.
In Minkowski spacetime it is the open double cone between p and q, empty unless p ≪ q. The
chronological diamonds are the members of alexandrovBasis and the regions of the Haag–Kastler
net.
Blueprint: def:causal-diamond
🔗def
The causal diamond J⁺(p) ∩ J⁻(q) of two points: the points x with p ≺ x and x ≺ q.
It is causally convex (causalDiamond_isCausallyConvex) and contains the chronological diamond
(chronologicalDiamond_subset_causalDiamond). Since ≺ is reflexive, it contains p and q whenever
p ≺ q; in Minkowski spacetime it is the closed double cone between p and q.
Blueprint: def:causal-diamond
The structure lemmas of the causal diamond all follow from transitivity of \prec. Enlarging the
vertices enlarges the diamond (causalDiamond_subset_of, proved step by step in the
tutorial),
a nonempty diamond has p \prec q, and the diamond is causally convex:
open Physicslib4 Spacetime in
Physicslib4.Spacetime.causallyPrecedes_of_causalDiamond_nonempty (M : Spacetime) (t : M.TimeOrientation)
{p q : M.Carrier} (h : (M.causalDiamond t p q).Nonempty) : p ≺[M, t] q#check causallyPrecedes_of_causalDiamond_nonempty
Physicslib4.Spacetime.causallyPrecedes_of_causalDiamond_nonempty (M : Spacetime) (t : M.TimeOrientation)
{p q : M.Carrier} (h : (M.causalDiamond t p q).Nonempty) : p ≺[M, t] q
🔗def
A region C is causally convex: it contains every point causally between two of its points,
so p, r ∈ C with p ≺ q ≺ r give q ∈ C.
Informally, every causal curve that leaves C never returns to it. Causal diamonds and causally
complete regions are causally convex (causalDiamond_isCausallyConvex,
LorentzianSpacetime.isCausallyConvex_of_isCausallyComplete).
Blueprint: def:causally-convex-region
open Physicslib4 Spacetime in
Physicslib4.Spacetime.causalDiamond_isCausallyConvex (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) :
M.IsCausallyConvex t (M.causalDiamond t p q)#check causalDiamond_isCausallyConvex
Physicslib4.Spacetime.causalDiamond_isCausallyConvex (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) :
M.IsCausallyConvex t (M.causalDiamond t p q)
The chronological diamond lies inside the causal one
(chronologicalDiamond_subset_causalDiamond). The family of all chronological diamonds is
alexandrovBasis M t, and its members are exactly the sets chronologicalDiamond M t p q
(mem_alexandrovBasis_iff_eq_chronologicalDiamond). The topology they generate:
🔗def
The Alexandrov topology of a spacetime with a time orientation: the topology generated by the
chronological diamonds I⁺(p) ∩ I⁻(q).
It is defined by the causal structure alone, without reference to the manifold topology. On
standard Minkowski spacetime it equals the Euclidean topology of ℝ⁴
(alexandrov_eq_euclidean_standardMinkowski), and the diamonds form a basis
(isTopologicalBasis_alexandrovBasis_standardMinkowski). In general it need not be Hausdorff; a
Lorentzian spacetime (LorentzianSpacetime) is a spacetime with a time orientation whose
Alexandrov topology is Hausdorff, and there the diamonds form a basis whenever they have the
intersection property: every point of the intersection of two diamonds lies in a diamond inside
that intersection (LorentzianSpacetime.isTopologicalBasis_alexandrovBasis, for a spacetime
with two points or more). In the standard theory the intersection property holds in every
spacetime, since chronological futures are open in the manifold topology; this is not proved in
the library, so the theorem takes it as the hypothesis hdir.
Implementation note: TopologicalSpace.generateFrom treats alexandrovBasis as a subbasis; that
it is a basis is a theorem. The topology is a reducible def, not an instance, so that it does
not compete with the manifold topology Spacetime.topology on the same type;
MinkowskiSpacetime is built on the type synonym MinkowskiSpacetimeCarrier, which carries it
as an instance.
Blueprint: def:alexandrov-topology
A Lorentzian spacetime bundles a spacetime, a time orientation and the Hausdorff condition:
🔗structure
A Lorentzian spacetime: a spacetime with a time orientation whose Alexandrov topology is
Hausdorff.
It bundles a spacetime (toSpacetime), a time orientation t (timeOrientation), and the
condition that the Alexandrov topology, generated by the diamonds I⁺(p) ∩ I⁻(q) for t, is
Hausdorff (alexandrov_t2). The Hausdorff condition is a causality condition: it is equivalent
to strong causality, and to the Alexandrov topology agreeing with the manifold topology (the
theorem "Properties of the Alexandrov Topology" of the blueprint's chapter 9, which is context
and is not formalised). It holds for Minkowski spacetime
(alexandrov_eq_euclidean_standardMinkowski).
The causal notions of Spacetime are restated for the bundled time orientation, for example
LorentzianSpacetime.IsBasisSet, LorentzianSpacetime.IsCompletelySpacelike and
LorentzianSpacetime.spacelikeComplement. The Haag–Kastler axioms in curved spacetime are stated
over an abstract interface, AQFT.HaagKastlerCurved.LorentzianSpacetime, which this structure
instantiates through LorentzianSpacetime.toAbstractIdentityComponent.
Blueprint: def:lorentzian-spacetime
Fields
toSpacetime : Spacetime
The underlying spacetime: a connected four-dimensional manifold with a Lorentzian
metric.
timeOrientation : self.toSpacetime.TimeOrientation
The time orientation t: a smooth, nowhere-vanishing, everywhere timelike vector field
that fixes the future half of each light cone.
alexandrov_t2 : T2Space self.toSpacetime.Carrier
The Alexandrov topology for t, generated by the diamonds I⁺(p) ∩ I⁻(q), is Hausdorff.
This is equivalent to strong causality, and to the Alexandrov topology agreeing with the
manifold topology (a standard result, not formalised here).
On it, the diamonds form a basis under the intersection hypothesis hdir; the covering
condition is proved from the Hausdorff field (sUnion_alexandrovBasis_eq_univ), and needs at least
two points:
open Physicslib4 Spacetime LorentzianSpacetime in
Physicslib4.Spacetime.LorentzianSpacetime.isTopologicalBasis_alexandrovBasis (M : LorentzianSpacetime)
[Nontrivial M.Carrier]
(hdir :
∀ B₁ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation,
∀ B₂ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation,
∀ x ∈ B₁ ∩ B₂, ∃ B₃ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation, x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂) :
TopologicalSpace.IsTopologicalBasis (M.toSpacetime.alexandrovBasis M.timeOrientation)#check isTopologicalBasis_alexandrovBasis
Physicslib4.Spacetime.LorentzianSpacetime.isTopologicalBasis_alexandrovBasis (M : LorentzianSpacetime)
[Nontrivial M.Carrier]
(hdir :
∀ B₁ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation,
∀ B₂ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation,
∀ x ∈ B₁ ∩ B₂, ∃ B₃ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation, x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂) :
TopologicalSpace.IsTopologicalBasis (M.toSpacetime.alexandrovBasis M.timeOrientation)
Lean's printer hides the topology argument of IsTopologicalBasis: it is the Alexandrov topology,
which the source passes explicitly with @.
5.3.5. Minkowski space🔗
Blueprint: def:standard-minkowski-spacetime, def:minkowski-spacetime,
lmm:minkowski-chronological-open, thrm:minkowski-alexandrov-basis,
lmm:minkowski-diamonds-upward-directed.
🔗def
Standard Minkowski spacetime: ℝ⁴ with its Euclidean topology and the constant metric
diag(-1, 1, 1, 1).
The metric is η(v, w) = -v⁰w⁰ + v¹w¹ + v²w² + v³w³ at every point, in the standard coordinates
(minkowskiForm). Its usual time orientation is the constant field ∂₀
(standardMinkowskiTimeOrientation); its geodesics are the straight lines traversed at constant
velocity (standardMinkowski_isGeodesic_iff), and I⁺(p) is the open forward light cone of p
(chronologicalFuture_standardMinkowski). The Haag–Kastler axioms in Minkowski spacetime are
stated on this spacetime.
Implementation note: the atlas is the single identity chart of EuclideanSpace ℝ (Fin 4) and
the model with corners is the identity, so a tangent space is ℝ⁴ itself.
Blueprint: def:standard-minkowski-spacetime
🔗def
The standard time orientation of Minkowski spacetime: the constant vector field ∂₀ = e₀.
With it, a timelike vector v is future-pointing exactly when its time component v⁰ is positive.
All the causal notions of standard Minkowski spacetime in the library (≪, ≺, the diamonds, the
Alexandrov topology and the Haag–Kastler axioms) use this time orientation.
Blueprint: def:lorentz-path
🔗def
Minkowski spacetime: standard Minkowski spacetime with the Alexandrov topology as its topology.
The Alexandrov topology, generated by the diamonds I⁺(p) ∩ I⁻(q), equals the Euclidean topology
of ℝ⁴ (alexandrov_eq_euclidean_standardMinkowski), so this is the same spacetime as
StandardMinkowskiSpacetime with its topology described causally.
Implementation note: the carrier is the type synonym MinkowskiSpacetimeCarrier of ℝ⁴, whose
TopologicalSpace instance is the Alexandrov topology. The charts, smooth structure, Hausdorff
property and connectedness are transported along the identity homeomorphism
euclideanHomeoMinkowski (instances instChartedSpaceMinkowskiCarrier and
instIsManifoldMinkowskiCarrier), and the metric is minkowskiForm.
Blueprint: def:minkowski-spacetime
With the curve-based definitions, the chronological future of a point is the open forward light
cone, I^+(p) = \{q : \eta(q-p, q-p) < 0,\ q^0 > p^0\} (minkowskiForwardCone). The inclusion
\subseteq integrates the velocity along each trip segment; the inclusion \supseteq uses the
straight segment from p to q, a geodesic.
open Physicslib4 Spacetime in
Physicslib4.chronologicalFuture_standardMinkowski (p : SpacetimeModel) :
StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p = minkowskiForwardCone p#check chronologicalFuture_standardMinkowski
Physicslib4.chronologicalFuture_standardMinkowski (p : SpacetimeModel) :
StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p = minkowskiForwardCone p
From the cone description, the Alexandrov topology of standard Minkowski space is its Euclidean
topology (inferInstance in the statement is the Euclidean topology of \mathbb{R}^4):
open Physicslib4 Spacetime in
Physicslib4.alexandrov_eq_euclidean_standardMinkowski :
StandardMinkowskiSpacetime.alexandrovTopology standardMinkowskiTimeOrientation = inferInstance#check alexandrov_eq_euclidean_standardMinkowski
Physicslib4.alexandrov_eq_euclidean_standardMinkowski :
StandardMinkowskiSpacetime.alexandrovTopology standardMinkowskiTimeOrientation = inferInstance
The diamonds of Minkowski space have the intersection property
(alexandrovBasis_exists_subset_inter_standardMinkowski), so they form a basis of the Alexandrov
topology without hypotheses
(isTopologicalBasis_alexandrovBasis_standardMinkowski).
They are also upward directed: any two lie in a common diamond, whose vertices are a common
chronological past point and a common chronological future point of theirs.
open Physicslib4 Spacetime in
Physicslib4.Spacetime.alexandrovBasis_directed {B₁ B₂ : Set SpacetimeModel}
(h₁ : B₁ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation)
(h₂ : B₂ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) :
∃ B ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation, B₁ ⊆ B ∧ B₂ ⊆ B#check alexandrovBasis_directed
Physicslib4.Spacetime.alexandrovBasis_directed {B₁ B₂ : Set SpacetimeModel}
(h₁ : B₁ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation)
(h₂ : B₂ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) :
∃ B ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation, B₁ ⊆ B ∧ B₂ ⊆ B
The geodesics of standard Minkowski space are the paths with zero acceleration, so the straight
lines traversed at constant velocity
(standardMinkowski_isGeodesic_iff),
because its Levi-Civita connection is the ordinary derivative of the components
(standardMinkowski_leviCivita_apply).
5.3.6. Causal complements🔗
Blueprint: def:spacelike-complement, lmm:spacelike-complement-order,
def:causal-closure, def:causally-complete-region,
thrm:causally-complete-lattice, thrm:causal-complement-de-morgan,
thrm:causally-complete-convex.
The lattice theory is stated on a Lorentzian spacetime, with its own time orientation;
Spacetime.spacelikeComplement M t is the same set for an explicit time orientation.
🔗def
The spacelike complement B⊥ of a region B of a Lorentzian spacetime: the points spacelike
related to every point of B.
By Einstein causality, observables localised in B⊥ commute with those localised in B: B⊥ is the
geometric side of locality and of Haag duality. Complementation is antitone
(spacelikeComplement_antitone), B ⊆ B⊥⊥ (subset_spacelikeComplement_spacelikeComplement),
B⊥⊥⊥ = B⊥ (spacelikeComplement_spacelikeComplement_spacelikeComplement) and B ∩ B⊥ = ∅
(disjoint_spacelikeComplement). Moreover B₁ ⊆ B₂⊥ exactly when B₁ and B₂ are completely
spacelike (subset_spacelikeComplement_iff), so complementation is the Galois connection of the
relation "spacelike related". The spacelike complement of the whole spacetime is empty
(spacelikeComplement_univ), and that of the empty set is the whole spacetime.
Blueprint: def:spacelike-complement
🔗def
The causal closure B ↦ B⊥⊥ of a region: its double spacelike complement, as a closure
operator.
The causal closure is monotone, extensive (B ⊆ B⊥⊥) and idempotent (B⊥⊥⊥⊥ = B⊥⊥). Physically,
B⊥⊥ is the largest region whose physics is determined by B through causality. In Minkowski
spacetime, for example, the causal closure of a ball in a time slice is the double cone over the
ball (a standard fact, not formalised here).
Implementation note: Mathlib's ClosureOperator bundles the three laws as fields, so they are
proved in constructing this term, from spacelikeComplement_antitone,
subset_spacelikeComplement_spacelikeComplement and
spacelikeComplement_spacelikeComplement_spacelikeComplement; causalClosure_apply unfolds it
to B⊥⊥.
Blueprint: def:causal-closure
🔗def
A region B is causally complete: it equals its causal closure, B⊥⊥ = B.
The causally complete regions are the fixed points of causalClosure
(isCausallyComplete_iff_isClosed). Every spacelike complement B⊥ is causally complete
(isCausallyComplete_spacelikeComplement), causally complete regions are closed under
intersections and are causally convex (isCausallyConvex_of_isCausallyComplete). They are a
common choice of index set for the local algebras of algebraic quantum field theory; the
Haag–Kastler net of the library is indexed by diamonds instead.
Blueprint: def:causally-complete-region
🔗def
The type of causally complete regions of a Lorentzian spacetime, ordered by inclusion.
They form a complete lattice: the meet is the intersection, and the join of a family is the
causal closure of its union. The causal complement B ↦ B⊥ (causalComplement) is an
orthocomplementation of this lattice: an order-reversing involution with B ⊓ B⊥ = ⊥ and
B ⊔ B⊥ = ⊤ (inf_causalComplement, sup_causalComplement), so the De Morgan laws hold
(causalComplement_sup, causalComplement_iSup, ...).
Implementation note: the type is Mathlib's ClosureOperator.Closeds of causalClosure, so an
element is a pair of a set B and a proof that B⊥⊥ = B. The CompleteLattice instance is
transported from the closure operator along its Galois insertion
(ClosureOperator.gi) and is anonymous.
Blueprint: thrm:causally-complete-lattice
🔗def
The causal complement of a causally complete region B: its spacelike complement B⊥, again
causally complete.
On the lattice CausallyCompleteRegion it is an order-reversing involution, (B⊥)⊥ = B
(causalComplement_causalComplement, causalComplement_antitone), and an orthocomplement:
B ⊓ B⊥ = ⊥ and B ⊔ B⊥ = ⊤ (inf_causalComplement, sup_causalComplement). The underlying set is
spacelikeComplement (causalComplement_coe).
Blueprint: thrm:causally-complete-lattice
The orthocomplement laws. Their proofs use that \mathbf{B} \cap \mathbf{B}^\perp = \emptyset,
which rests on the reflexivity of \prec, and the set-level De Morgan law
(\mathbf{B}_1 \cup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \cap \mathbf{B}_2^\perp:
open Physicslib4 Spacetime in
Physicslib4.Spacetime.LorentzianSpacetime.inf_causalComplement (M : LorentzianSpacetime)
(B : M.CausallyCompleteRegion) : B ⊓ M.causalComplement B = ⊥#check LorentzianSpacetime.inf_causalComplement
Physicslib4.Spacetime.LorentzianSpacetime.inf_causalComplement (M : LorentzianSpacetime)
(B : M.CausallyCompleteRegion) : B ⊓ M.causalComplement B = ⊥
open Physicslib4 Spacetime in
Physicslib4.Spacetime.LorentzianSpacetime.sup_causalComplement (M : LorentzianSpacetime)
(B : M.CausallyCompleteRegion) : B ⊔ M.causalComplement B = ⊤#check LorentzianSpacetime.sup_causalComplement
Physicslib4.Spacetime.LorentzianSpacetime.sup_causalComplement (M : LorentzianSpacetime)
(B : M.CausallyCompleteRegion) : B ⊔ M.causalComplement B = ⊤
The De Morgan laws are causalComplement_sup, causalComplement_inf and their infinitary forms
causalComplement_iSup and causalComplement_iInf. Every causally complete region is causally
convex (isCausallyConvex_of_isCausallyComplete), as is every causal diamond
(causalDiamond_isCausallyConvex).
5.3.7. The Lorentz group and isometries🔗
Blueprint: def:lorentz-transformation, lmm:lorentz-closure,
def:inhomogeneous-lorentz-group, def:lorentz-path,
thrm:causal-precedence-lorentz-invariant, lmm:isometry-preserves-chronology,
lmm:isometry-preserves-basis-sets.
The three conditions on a linear automorphism of \mathbb{R}^4:
🔗def
An invertible linear map Λ of ℝ⁴ is a Lorentz transformation: it preserves the Minkowski
form, η(Λv, Λw) = η(v, w).
Lorentz transformations are the linear isometries of Minkowski spacetime: rotations, boosts,
parity and time reversal, and their products. With IsProper and IsOrthochronous they give
the proper orthochronous Lorentz group SO(1,3)↑, the Λ of the inhomogeneous Lorentz group.
Blueprint: def:lorentz-transformation
🔗def
An invertible linear map Λ of ℝ⁴ is proper: det Λ = 1.
A Lorentz transformation has det Λ = ±1; the proper ones exclude parity and time reversal
individually, but not their product.
Blueprint: def:lorentz-transformation
🔗def
An invertible linear map Λ of ℝ⁴ is orthochronous: it preserves the direction of time,
(Λe₀)⁰ > 0.
Here e₀ = (1, 0, 0, 0) is the unit time vector. An orthochronous Lorentz transformation sends
every future-pointing timelike vector to a future-pointing timelike vector
(isOrthochronous_pos_time_of_timelike).
Blueprint: def:lorentz-transformation
Their closure properties are isLorentz_trans, isLorentz_symm and the like. The group
AQFT.HaagKastler.InhomogeneousLorentzGroup of pairs (\Lambda, a) is shown in the
Haag–Kastler chapter.
Its action on smooth paths:
🔗def
The Lorentz pushforward g μ of a smooth path in standard Minkowski spacetime, for
g = (Λ, a) in the inhomogeneous Lorentz group: s ↦ Λμ(s) + a.
The parameter space is unchanged and the velocity is Λμ̇(s) (lorentzPath_mfderivWithin), non-zero
because Λ is invertible. The pushforward of a causal, future-oriented geodesic is again one, with
endpoints g·p and g·q (lorentzPath_isCausal, lorentzPath_isFutureOriented,
lorentzPath_isGeodesic), so causal precedence is Poincaré invariant: g·p ≺ g·q exactly when
p ≺ q (causallyPrecedes_smul_iff). It is the Minkowski counterpart of the pushforward of a path
under an isometry (Spacetime.Isometry.pushforwardPath).
Blueprint: def:lorentz-path
The pushforward of a causal trip segment is a causal trip segment, so chains go to chains, and the
inverse gives the converse:
open Physicslib4 Spacetime in
Physicslib4.causallyPrecedes_smul_iff (g : AQFT.HaagKastler.InhomogeneousLorentzGroup)
(p q : StandardMinkowskiSpacetime.Carrier) :
(g • p ≺[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] g • q) ↔
p ≺[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] q#check causallyPrecedes_smul_iff
Physicslib4.causallyPrecedes_smul_iff (g : AQFT.HaagKastler.InhomogeneousLorentzGroup)
(p q : StandardMinkowskiSpacetime.Carrier) :
(g • p ≺[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] g • q) ↔
p ≺[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] q
The same holds for \ll (chronologicallyPrecedes_smul_iff); spacelike separation and complete
spacelike separation are invariant (isSpacelikeRelated_smul_iff,
isCompletelySpacelike_smul_iff); and the group maps diamonds to diamonds
(isAlexandrovBasisSet_smul). Tutorial
chapter 3 proves
causallyPrecedes_smul_iff from the segment lemma.
For a general spacetime the symmetries are the isometries:
🔗structure
An isometry of a spacetime: a C^∞ diffeomorphism φ of M whose differential preserves the
metric, g_(φ(x))(dφ_x v, dφ_x w) = g_x(v, w).
Isometries are the symmetries of the geometry; for Minkowski spacetime they include the Poincaré
transformations. They form a group under composition, (φ * ψ)(x) = φ(ψ(x)), acting faithfully on
the points of M (g • x). An isometry preserves the causal type of tangent vectors
(isTimelike_mfderiv_iff), but it may reverse the time orientation. The isometries "connected to
the identity" of Axiom 5 are the subgroup identityComponent, and those that also preserve the
time orientation are orientedIdentityComponent.
Implementation note: the diffeomorphism is Mathlib's Diffeomorph, so smoothness of φ and φ⁻¹ is
built in, and dφ_x is the manifold derivative mfderiv.
Blueprint: lmm:isometry-preserves-classification (isometries are described in
lmm:isometry-pullback-metric)
Fields
preserves : ∀ (x : M.Carrier) (v w : TangentSpace M.model x),
((M.val (self.toDiffeo x)) ((mfderiv% ⇑self.toDiffeo x) v)) ((mfderiv% ⇑self.toDiffeo x) w) = ((M.val x) v) w
φ preserves the metric: g_(φ(x))(dφ_x v, dφ_x w) = g_x(v, w), with dφ_x the manifold
derivative mfderiv.
🔗def
The identity component of the isometry group: the connected component of the identity, for the
compact-open group topology.
These are the isometries "connected to the identity" of Axiom 5 in curved spacetime. For
Minkowski spacetime they are the proper orthochronous Poincaré transformations, while parity and
time reversal lie in other components (a standard fact, not formalised here). Every isometry in
the identity component preserves the time orientation, but the proof needs a Myers–Steenrod-type
rigidity theorem that Mathlib does not provide; the axioms therefore use
orientedIdentityComponent, which is the same group with orientation preservation built into
its definition.
Implementation note: the group topology is induced by g ↦ (g, g⁻¹) into C(M, M) × C(M, M), with
the compact-open topology on each factor; using both g and g⁻¹ makes inversion continuous, and
local compactness of M makes composition continuous, so IsTopologicalGroup holds and the
connected component of 1 is a subgroup (Subgroup.connectedComponentOfOne).
An isometry preserves the causal type of vectors (Isometry.isTimelike_mfderiv_iff and its null
and spacelike companions), and pushes smooth paths forward (Isometry.pushforwardPath). If it
also preserves the future orientation, it maps trips to trips:
🔗def
An isometry g preserves the future orientation t: its differential sends future-pointing
tangent vectors to future-pointing tangent vectors.
Such an isometry carries trips to trips, so p ≪ q implies g(p) ≪ g(q)
(chronologicallyPrecedes_pushforward). The property holds for the identity and is closed under
composition; the subgroup asks it of g and of g⁻¹ (futureOrientationPreserving).
Blueprint: lmm:isometry-preserves-chronology
🔗def
The oriented identity component: the isometries in the identity component that preserve the
time orientation t.
This is the group of "isometries connected to the identity" of Axiom 5 in curved spacetime, the
group Isom of LorentzianSpacetime.toAbstractIdentityComponent. Its members carry trips to
trips and chronological diamonds to chronological diamonds, with
φ(I⁺(p) ∩ I⁻(q)) = I⁺(φ(p)) ∩ I⁻(φ(q))
(alexandrovBasis_image_of_mem_orientedIdentityComponent), which is what makes the Axiom 5 maps
𝔘(B) → 𝔘(φ(B)) well defined.
Implementation note: the group is identityComponent intersected with
futureOrientationPreserving. Every isometry in the identity component preserves the future
orientation, so the intersection is the whole identity component, but the proof needs a
Myers–Steenrod-type rigidity theorem that Mathlib does not provide, so orientation preservation
is part of the definition instead.
Blueprint: lmm:isometry-preserves-basis-sets
Every member of the oriented identity component maps diamonds to diamonds, which is what makes the
curved-spacetime Axiom 5 maps \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(\varphi(\mathbf{B}))
well defined. In the statement, ⇑g.toDiffeo '' B is the image \varphi(\mathbf{B}):
open Physicslib4 Spacetime Isometry in
Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem_orientedIdentityComponent {M : Spacetime} (g : M.Isometry)
(t : M.TimeOrientation) (hg : g ∈ orientedIdentityComponent M t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) :
⇑g.toDiffeo '' B ∈ M.alexandrovBasis t#check
alexandrovBasis_image_of_mem_orientedIdentityComponent
Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem_orientedIdentityComponent {M : Spacetime} (g : M.Isometry)
(t : M.TimeOrientation) (hg : g ∈ orientedIdentityComponent M t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) :
⇑g.toDiffeo '' B ∈ M.alexandrovBasis t
The proof is \varphi(I^\pm(p)) = I^\pm(\varphi(p)) (Isometry.chronologicalFuture_image,
Isometry.chronologicalPast_image) and injectivity of \varphi. The curved-spacetime axioms
(Section 10.7
of the blueprint) use this group through LorentzianSpacetime.toAbstractIdentityComponent.
5.3.8. The Levi-Civita connection and geodesics🔗
Blueprint: def:pseudo-riemannian-metric, def:metric-compatible-connection,
def:levi-civita-connection, thrm:levi-civita-exists-unique,
lmm:minkowski-levi-civita-flat, lmm:isometry-preserves-geodesics.
The metric, of any signature, on a manifold M modelled by I:
🔗structure
A pseudo-Riemannian metric on a manifold M: a smooth field of symmetric, non-degenerate
bilinear forms g_x on the tangent spaces TₓM.
No signature is imposed, so Riemannian and Lorentzian metrics are both examples; the metric of
a spacetime is one (Spacetime.toPseudoRiemannianMetric). Non-degeneracy makes v ↦ g_x(v, ·) an
isomorphism of TₓM onto its dual (bijective_val, flatEquiv), the index lowering of physics
notation. The Levi-Civita connection and geodesics are built on this structure
(PseudoRiemannianMetric.leviCivita), and they do not use the signature.
Implementation note: Mathlib's Bundle.ContMDiffRiemannianMetric requires positivity, so it is
not reused; the field contMDiff has the same bundle-section shape as its smoothness field.
Blueprint: def:pseudo-riemannian-metric
Fields
val : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
The metric g: at each point x, a continuous bilinear form g_x on TₓM.
symm : ∀ (x : M) (v w : TangentSpace I x), ((self.val x) v) w = ((self.val x) w) v
g is symmetric: g_x(v, w) = g_x(w, v).
nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ (w : TangentSpace I x), ((self.val x) v) w = 0) → v = 0
g is non-degenerate: if g_x(v, w) = 0 for every w, then v = 0.
contMDiff : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ↑⊤ fun x => ⟨x, self.val x⟩
g is smooth: a C^∞ section of the bundle of continuous bilinear forms on the tangent
bundle.
Connections are Mathlib's CovariantDerivative, and the two conditions on them are:
🔗def
A covariant derivative ∇ on the tangent bundle is compatible with the metric g: the Leibniz
rule X(g(σ, τ)) = g(∇_X σ, τ) + g(σ, ∇_X τ) holds.
The left side is the derivative of the function y ↦ g_y(σ(y), τ(y)) at x in the direction
X(x); the identity is asked at every point x where X, σ and τ are differentiable. In index
notation it is ∇μ g(νρ) = 0: parallel transport preserves inner products, and so the causal
type of vectors.
Implementation note: this is Mathlib's condition CovariantDerivative.isMetricCompatible_iff
with g in place of the inner product. The covariant derivative is Mathlib's
CovariantDerivative, a map sending a vector field Y to the field of linear maps
(∇Y)_x : TₓM → TₓM, with ∇_X Y at x given by (∇Y)_x(X(x)).
Blueprint: def:metric-compatible-connection
🔗structure
A covariant derivative is a Levi-Civita connection of the metric g: it is torsion-free and
compatible with g.
Torsion-free means ∇X Y - ∇Y X = [X, Y] for vector fields differentiable at the point, so the
Christoffel symbols are symmetric, Γ^ρ(μν) = Γ^ρ(νμ). Every pseudo-Riemannian metric has a
Levi-Civita connection (PseudoRiemannianMetric.exists_isLeviCivitaFor), and two of them agree
on differentiable vector fields (IsLeviCivitaFor.uniqueness); the Koszul formula expresses it
through g (IsLeviCivitaFor.koszul).
Implementation note: the structure mirrors Mathlib's CovariantDerivative.IsLeviCivitaConnection,
with g in place of the inner product. Uniqueness holds only on differentiable vector fields,
since a covariant derivative is unconstrained on the others.
Blueprint: def:levi-civita-connection
Fields
torsion : cov.torsion = 0
∇ is torsion-free: its torsion T(X, Y) = ∇_X Y - ∇_Y X - [X, Y] vanishes.
Existence is the Koszul construction, koszulConnection:
open Physicslib4 Geometry in
Physicslib4.Geometry.PseudoRiemannianMetric.exists_isLeviCivitaFor.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
[ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) :
∃ cov, IsLeviCivitaFor g cov#check PseudoRiemannianMetric.exists_isLeviCivitaFor
Physicslib4.Geometry.PseudoRiemannianMetric.exists_isLeviCivitaFor.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
[ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) :
∃ cov, IsLeviCivitaFor g cov
Uniqueness compares two Levi-Civita connections through the Koszul formula
(IsLeviCivitaFor.koszul), which expresses 2g(\nabla_X Y, Z) through derivatives of g and
Lie brackets alone, and non-degeneracy. The hypothesis hY is differentiability of Y at x.
(IsManifold I (↑⊤) M is Lean's rendering of a C^\infty manifold.)
open Physicslib4 Geometry in
Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor.uniqueness.{u_1, u_2, u_3} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E]
{g : PseudoRiemannianMetric I M} {cov cov' : CovariantDerivative I E (TangentSpace I)} (hcov : IsLeviCivitaFor g cov)
(hcov' : IsLeviCivitaFor g cov') {x : M} {Y : (x : M) → TangentSpace I x} (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
(X₀ : TangentSpace I x) : (↑cov Y x) X₀ = (↑cov' Y x) X₀#check CovariantDerivative.IsLeviCivitaFor.uniqueness
Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor.uniqueness.{u_1, u_2, u_3} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E]
{g : PseudoRiemannianMetric I M} {cov cov' : CovariantDerivative I E (TangentSpace I)} (hcov : IsLeviCivitaFor g cov)
(hcov' : IsLeviCivitaFor g cov') {x : M} {Y : (x : M) → TangentSpace I x} (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
(X₀ : TangentSpace I x) : (↑cov Y x) X₀ = (↑cov' Y x) X₀
The connection the library uses, chosen from the existence theorem:
🔗def
The Levi-Civita connection ∇ of the metric g.
It is torsion-free and compatible with g (isLeviCivitaFor_leviCivita), and any other connection
with these properties agrees with it on differentiable vector fields
(CovariantDerivative.IsLeviCivitaFor.uniqueness). In coordinates its Christoffel symbols are
Γ^ρ_(μν) = ½ g^(ρσ)(∂μ g(σν) + ∂ν g(σμ) - ∂σ g(μν)). Geodesics of a spacetime are defined
with it (Spacetime.IsGeodesic). For a constant metric on a vector space, as in Minkowski
spacetime, it is the ordinary directional derivative (leviCivita_apply_eq_fderiv).
Implementation note: the connection is a choice (Exists.choose) from
exists_isLeviCivitaFor, so its values on non-differentiable vector fields are unspecified;
statements about it use only differentiable fields.
Blueprint: thrm:levi-civita-exists-unique
On a vector space with a constant metric, such as standard Minkowski space, the ordinary
directional derivative Geometry.flatConnection is a Levi-Civita connection
(isLeviCivitaFor_flatConnection), so by uniqueness leviCivita is the ordinary derivative on
differentiable fields
(leviCivita_apply_eq_fderiv).
Isometries preserve the Levi-Civita connection, d\varphi\big(\nabla_{\varphi^*X}\varphi^*Y\big) =
\nabla_X Y at corresponding points (Isometry.mfderiv_leviCivita_mpullback), because every term of
the Koszul formula is natural under \varphi. Hence they map geodesics to geodesics; the converse
is the same statement for \varphi^{-1}:
open Physicslib4 Spacetime in
Physicslib4.Spacetime.Isometry.pushforwardPath_isGeodesic.{u_1} {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath)
(h : M.IsGeodesic μ) : M.IsGeodesic (g.pushforwardPath μ)#check Isometry.pushforwardPath_isGeodesic
Physicslib4.Spacetime.Isometry.pushforwardPath_isGeodesic.{u_1} {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath)
(h : M.IsGeodesic μ) : M.IsGeodesic (g.pushforwardPath μ)
The Minkowski counterpart, for lorentzPath, is lorentzPath_isGeodesic. The cross-metric form,
CrossIsometry.pushforwardPath_isGeodesic, is for a diffeomorphism carrying one metric to another,
\psi^* g_2 = g_1, as general covariance needs. The pullback metric \psi^* g and cross-metric
isometries (Pullback.lean, CrossMetricIsometry.lean) carry all the results above between two
spacetimes; they serve general covariance and are described with it.