Causality on a spacetime #
This file formalises the causal-relations vocabulary of section 10.5 of the
AQFT-in-Lean blueprint: trips, causal trips, the chronological precedence
relation ≪, the causal precedence relation ≺, and their associated
chronological/causal future/past sets.
Main definitions #
Physicslib4.Spacetime.IsGeodesic: a smooth path is an (affinely parametrised) geodesic of the Levi-Civita connection of the spacetime metric (Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean), stated without charts.Physicslib4.Spacetime.IsTrip/IsCausalTrip: a trip / causal trip is a smooth curve which is piecewise a future-oriented timelike / causal geodesic, with designated past and future endpoints.Physicslib4.Spacetime.ChronologicallyPrecedes(≪): the existence of a trip fromptoq; it is strict.Physicslib4.Spacetime.CausallyPrecedes(≺):p = qor there is a causal trip fromptoq; it is reflexive, sop ∈ J^±(p).Physicslib4.Spacetime.chronologicalFuture/chronologicalPast,causalFuture/causalPast: pointwise and set-valued versions.Physicslib4.Spacetime.IsSpacelikeRelated,IsCompletelySpacelike: the spacelike-relatedness vocabulary.
Modelling notes #
Mathlib has no geodesics and only a Riemannian Levi-Civita connection.
IsGeodesicuses the pseudo-Riemannian Levi-Civita connection ofPhysicslib4.Geometryand imposes the geodesic condition at interior parameters of the path through vector fields extending its velocity;Physicslib4/Spacetime/AlongPath.leanshows this is well defined and non-vacuous.The "piecewise" condition on trips is encoded by partitioning the parameter space into finitely many sub-intervals on each of which the smooth curve restricts to a future-oriented timelike (resp. causal) geodesic.
Geodesics #
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Trips and chronological precedence #
A trip segment from p to q: a smooth curve with a representative that is a future-oriented timelike geodesic from p to q.
The representative path μ is timelike, future-oriented for the time orientation t, a geodesic
(IsGeodesic), and has past endpoint p and future endpoint q; so its parameter space is a
compact interval [a, b], with μ(a) = p and μ(b) = q. Physically, it is the worldline of a
free-falling massive particle from p to q. A trip is a finite chain of trip segments (IsTrip).
Blueprint: def:trip
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-segment chronological precedence: some trip segment runs from p to q.
Chronological precedence ≪ is the transitive closure of this relation (IsTrip).
Equations
- M.SegmentPrecedes t p q = ∃ (c : M.SmoothCurve), M.IsTripSegment t p q c
Instances For
There is a trip from p to q: a finite chain of one or more trip segments, joined at matching endpoints.
That is, there are points p = x₀, x₁, …, xₙ = q with n ≥ 1, each consecutive pair joined by a
future-oriented timelike geodesic segment (SegmentPrecedes). A trip is a broken timelike
geodesic, so concatenating trips gives a trip, and chronological precedence is transitive
(chronologicallyPrecedes_trans).
Implementation note: the chain is the transitive closure Relation.TransGen of
SegmentPrecedes; the trip is not stored as a curve.
Blueprint: def:trip
Equations
- M.IsTrip t p q = Relation.TransGen (M.SegmentPrecedes t) p q
Instances For
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
Equations
- M.ChronologicallyPrecedes t p q = M.IsTrip t p q
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Causal trips and causal precedence #
A causal trip segment from p to q: a smooth curve with a representative that is a future-oriented causal geodesic from p to q.
This is IsTripSegment with "timelike" weakened to "causal": the velocity is timelike or null
at every parameter (and never zero). Physically, it is the worldline of a free-falling particle,
massive or massless, from p to q.
Blueprint: def:causal-trip
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-segment causal precedence: some causal trip segment runs from p to q.
Causal trips are chains of one or more such steps (IsCausalTrip), and causal precedence ≺
allows chains of zero or more (CausallyPrecedes).
Equations
- M.CausalSegmentPrecedes t p q = ∃ (c : M.SmoothCurve), M.IsCausalTripSegment t p q c
Instances For
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
Equations
- M.IsCausalTrip t p q = Relation.TransGen (M.CausalSegmentPrecedes t) p q
Instances For
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
Equations
- M.CausallyPrecedes t p q = Relation.ReflTransGen (M.CausalSegmentPrecedes t) p q
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chronological and causal futures and pasts #
The chronological future I⁺(p) = {q | p ≪ q} of a point p.
In standard Minkowski spacetime I⁺(p) is the open future light cone of p
(chronologicalFuture_standardMinkowski). When there is no closed causal curve, p ∉ I⁺(p).
Blueprint: def:chronological-future-and-chronological-past
Equations
- M.chronologicalFuture t p = {q : M.Carrier | M.ChronologicallyPrecedes t p q}
Instances For
The chronological past I⁻(p) = {q | q ≪ p} of a point p.
Blueprint: def:chronological-future-and-chronological-past
Equations
- M.chronologicalPast t p = {q : M.Carrier | M.ChronologicallyPrecedes t q p}
Instances For
The chronological future I^+(S) of a set S, defined as
⋃ p ∈ S, I^+(p).
Equations
- M.chronologicalFutureSet t S = ⋃ p ∈ S, M.chronologicalFuture t p
Instances For
The chronological past I^-(S) of a set S, defined as
⋃ p ∈ S, I^-(p).
Equations
- M.chronologicalPastSet t S = ⋃ p ∈ S, M.chronologicalPast t p
Instances For
The causal future J⁺(p) = {q | p ≺ q} of a point p.
Since ≺ is reflexive, p ∈ J⁺(p). It contains the chronological future I⁺(p)
(chronologicalFuture_subset_causalFuture). In Minkowski spacetime J⁺(p) is the closed future
light cone of p, the points reached from p by a future-directed timelike or null straight line,
together with p itself.
Blueprint: def:causal-future-and-causal-past
Equations
- M.causalFuture t p = {q : M.Carrier | M.CausallyPrecedes t p q}
Instances For
The causal past J⁻(p) = {q | q ≺ p} of a point p.
Since ≺ is reflexive, p ∈ J⁻(p).
Blueprint: def:causal-future-and-causal-past
Equations
- M.causalPast t p = {q : M.Carrier | M.CausallyPrecedes t q p}
Instances For
The causal future J^+(S) of a set S, defined as
⋃ p ∈ S, J^+(p).
Equations
- M.causalFutureSet t S = ⋃ p ∈ S, M.causalFuture t p
Instances For
The causal past J^-(S) of a set S, defined as
⋃ p ∈ S, J^-(p).
Equations
- M.causalPastSet t S = ⋃ p ∈ S, M.causalPast t p
Instances For
Spacelike relatedness #
Two points are spacelike related: neither causally precedes the other, p₂ ∉ J⁺(p₁) ∪ J⁻(p₁).
No causal trip joins the two points in either direction, so no signal can pass between them.
The relation is symmetric (isSpacelikeRelated_comm). Since ≺ is reflexive, no point is
spacelike related to itself (isSpacelikeRelated_irrefl).
Blueprint: def:spacelike-related
Equations
- M.IsSpacelikeRelated t p₁ p₂ = (p₂ ∉ M.causalFuture t p₁ ∪ M.causalPast t p₁)
Instances For
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
Equations
- M.IsCompletelySpacelike t O₁ O₂ = ∀ p₁ ∈ O₁, ∀ p₂ ∈ O₂, M.IsSpacelikeRelated t p₁ p₂
Instances For
Chronological implies causal #
A timelike trip is in particular a causal trip, so chronological precedence refines causal precedence and chronological futures/pasts sit inside the corresponding causal ones.
A timelike path is causal.
Every trip segment is a causal trip segment.
Single-segment chronological precedence implies single-segment causal precedence.
Transitivity of chronological precedence. Two trips joined at a common
point q concatenate to a single (piecewise) trip: p ≪ q and q ≪ r give
p ≪ r. This is exactly the transitivity of the transitive closure.
Reflexivity of causal precedence. p ≺ p, by the trivial chain of no segments.
Causal precedence is equality or a (genuine) causal trip: p ≺ q ↔ p = q ∨ IsCausalTrip p q.
A causal trip from p to q gives causal precedence p ≺ q.
Transitivity of causal trips. Two causal trips joined at a common point concatenate.
Transitivity of causal precedence. p ≺ q and q ≺ r give p ≺ r.
A trip is a causal trip: chronological precedence gives a causal trip.
Chronological precedence implies causal precedence.
The chronological future is contained in the causal future.
The chronological past is contained in the causal past.
Causal-order refinements under the causality condition #
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
Equations
- M.NoClosedCausalCurve t = ∀ (p : M.Carrier), ¬M.IsCausalTrip t p p
Instances For
Under the causality condition, chronological precedence is irreflexive:
¬ (p ≪ p), because a trip from p to p is a forbidden closed causal trip.
Under the causality condition, causal trips are asymmetric: a causal trip from p
to q excludes one from q to p, since concatenation would give a closed causal trip.
Under the causality condition, causal precedence is antisymmetric:
p ≺ q → q ≺ p → p = q. If p ≠ q, both relations are causal trips, which
isCausalTrip_asymm excludes. Thus ≺ is a partial order.
Symmetry of spacelike relatedness #
Spacelike relatedness is irreflexive: p ∈ J^+(p), so no point is spacelike to itself.
Spacelike relatedness is symmetric.
Complete spacelike separation is symmetric in its two regions.
Complete spacelike separation is monotone under shrinking either region.
The empty region is completely spacelike to anything (on the left).
The empty region is completely spacelike to anything (on the right).
A union of regions is completely spacelike to O₂ iff each part is.
O₁ is completely spacelike to a union iff it is to each part.
Monotonicity of set-valued futures and pasts #
The set-valued chronological future is monotone.
The set-valued chronological past is monotone.
The set-valued causal future is monotone.
The set-valued causal past is monotone.
Alexandrov topology #
The Alexandrov basis: the family of all chronological diamonds I⁺(p) ∩ I⁻(q), for points p and q.
These sets generate the Alexandrov topology (alexandrovTopology), and they are the regions to
which the Haag–Kastler axioms assign local algebras. The family contains the empty set, for
example I⁺(p) ∩ I⁻(p) in a causal spacetime. Its members are exactly the sets
chronologicalDiamond t p q (mem_alexandrovBasis_iff_eq_chronologicalDiamond).
Blueprint: def:alexandrov-topology
Equations
- M.alexandrovBasis t = {U : Set M.Carrier | ∃ (p : M.Carrier) (q : M.Carrier), U = M.chronologicalFuture t p ∩ M.chronologicalPast t q}
Instances For
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
Equations
Instances For
Every basis set is open in the Alexandrov topology.
No-diamond points have only the whole space as neighbourhood. If x lies
in no Alexandrov diamond I⁺(p) ∩ I⁻(q), then every Alexandrov-open set (i.e. every
set generated from the diamond subbasis) containing x is the whole space M.
Openness of chronological futures and pasts #
Every set of the form I^+(p) ∩ I^-(q) is open in the Alexandrov topology.
This is the basis lemma restated on chronological futures and pasts.
If every point of I^+(p) has a chronological-future point (for all
x ∈ I^+(p) there exists b with x ≪ b), then the chronological future
I^+(p) is open in the Alexandrov topology.
Dually, if every point of I^-(p) has a chronological-past point (for all
x ∈ I^-(p) there exists a with a ≪ x), then the chronological past
I^-(p) is open in the Alexandrov topology.
Causal and chronological diamonds #
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
Equations
- M.causalDiamond t p q = M.causalFuture t p ∩ M.causalPast t q
Instances For
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
Equations
- M.chronologicalDiamond t p q = M.chronologicalFuture t p ∩ M.chronologicalPast t q
Instances For
Membership in the causal diamond: x ∈ J^+(p) ∩ J^-(q) iff p ≺ x and x ≺ q.
Membership in the chronological diamond: x ∈ I^+(p) ∩ I^-(q) iff p ≪ x and
x ≪ q.
Monotonicity under endpoint spread. If p' ≺ p and q ≺ q', then the causal
diamond of (p, q) is contained in the causal diamond of (p', q').
Causal convexity. If a, b lie in the causal diamond of (p, q), a ≺ z and
z ≺ b, then z lies in the causal diamond of (p, q).
A nonempty causal diamond forces p ≺ q.
The chronological diamond sits inside the causal diamond,
I^+(p) ∩ I^-(q) ⊆ J^+(p) ∩ J^-(q).
The Alexandrov basis is exactly the family of chronological diamonds: U is an
Alexandrov basis set iff U = I^+(p) ∩ I^-(q) for some p, q.
Causal convexity #
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
Equations
- M.IsCausallyConvex t C = ∀ ⦃p q r : M.Carrier⦄, p ∈ C → r ∈ C → M.CausallyPrecedes t p q → M.CausallyPrecedes t q r → q ∈ C
Instances For
Every causal diamond J^+(p) ∩ J^-(q) is a causally convex region.
The causally convex closure structure #
The whole spacetime is a causally convex region.
The empty region is causally convex (vacuously).
The intersection of two causally convex regions is causally convex.
An indexed intersection of causally convex regions is causally convex.
A set-indexed intersection of causally convex regions is causally convex.
The causal-convex hull of a region B: the smallest causally convex region
containing B, i.e. the intersection of all causally convex regions containing B.
Instances For
A region is contained in its causal-convex hull.
The causal-convex hull is causally convex.
Minimality / universal property. Any causally convex region containing B
contains the causal-convex hull of B.
The causal-convex hull is monotone.
The causal-convex hull fixes exactly the causally convex regions.
The causal-convex hull is idempotent.