Causality on a spacetime

This file formalises the causal-relations vocabulary of section 10.2 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 (placeholder): a Prop placeholder for "being a geodesic". Mathlib v4.31.0-rc1 does not provide a packaged notion of geodesic in a Lorentzian / pseudo-Riemannian manifold; we encode the predicate as an opaque Prop-valued definition (defined to True as a placeholder, see modelling notes).

• 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 (≪), Physicslib4.Spacetime.CausallyPrecedes (≺): the existence of a trip / causal trip from p to q.

• Physicslib4.Spacetime.chronologicalFuture / chronologicalPast, causalFuture / causalPast: pointwise and set-valued versions.

• Physicslib4.Spacetime.IsSpacelikeRelated, IsCompletelySpacelike: the spacelike-relatedness vocabulary.

Modelling notes

• Geodesics in Lorentzian manifolds are not packaged in Mathlib. We use a placeholder predicate IsGeodesic set to True; downstream agents should refine this to the genuine geodesic condition once Mathlib (or a sibling project) provides one. This is the only mathematical compromise in this file.

• 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 (placeholder)

def Physicslib4.Spacetime.IsGeodesic (M : Spacetime) (_μ : M.SmoothPath) : Prop

A geodesic of a spacetime, as needed by section 10.2 of the blueprint.

Mathlib v4.31.0-rc1 does not provide a Lorentzian / pseudo-Riemannian geodesic. We provide an opaque placeholder predicate. Downstream work should replace this by the genuine geodesic condition (typically: auto-parallelism of the tangent vector field along the curve with respect to the Levi-Civita connection of g).

Equations

• M.IsGeodesic _μ = True

Trips and chronological precedence

def Physicslib4.Spacetime.IsTripSegment (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) (c : M.SmoothCurve) : Prop

A trip segment from p to q in a spacetime M is a smooth curve c together with a representative smooth path μ that

• is future-oriented and timelike;
• is a geodesic;
• has past endpoint p and future endpoint q.

This is a single geodesic piece; a full (piecewise) trip is a finite chain of such segments (see IsTrip).

A TimeOrientation argument t is required to talk about future-orientation. The endpoints p, q : M.Carrier are given as parameters.

Equations

• One or more equations did not get rendered due to their size.

def Physicslib4.Spacetime.SegmentPrecedes (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

Single-segment chronological precedence: p and q are joined by one future-oriented timelike geodesic segment.

Equations

• M.SegmentPrecedes t p q = ∃ (c : M.SmoothCurve), M.IsTripSegment t p q c

def Physicslib4.Spacetime.IsTrip (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

A trip from p to q: a curve which is piecewise a future-oriented timelike geodesic, i.e. a finite chain of trip segments joined at matching endpoints. This is encoded as the transitive closure of single-segment precedence, which is exactly "there is a finite ascending sequence p = x₀, x₁, …, xₙ = q with each consecutive pair joined by a future-oriented timelike geodesic segment". This genuinely piecewise form is what makes chronological precedence transitive by concatenation.

Equations

• M.IsTrip t p q = Relation.TransGen (M.SegmentPrecedes t) p q

def Physicslib4.Spacetime.ChronologicallyPrecedes (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

Chronological precedence: p ≪ q iff there exists a trip from p to q, relative to a fixed time orientation.

Equations

• M.ChronologicallyPrecedes t p q = M.IsTrip t p q

def Physicslib4.Spacetime.«term_≪[_,_]_» : Lean.TrailingParserDescr

Chronological precedence: p ≪ q iff there exists a trip from p to q, relative to a fixed time orientation.

Equations

• One or more equations did not get rendered due to their size.

Causal trips and causal precedence

def Physicslib4.Spacetime.IsCausalTripSegment (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) (c : M.SmoothCurve) : Prop

A causal trip segment from p to q in a spacetime M is a smooth curve c together with a representative smooth path μ that

• is future-oriented and causal;
• is a (possibly degenerate) geodesic;
• has past endpoint p and future endpoint q.

Equations

• One or more equations did not get rendered due to their size.

def Physicslib4.Spacetime.CausalSegmentPrecedes (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

Single-segment causal precedence: p and q are joined by one future-oriented causal geodesic segment.

Equations

• M.CausalSegmentPrecedes t p q = ∃ (c : M.SmoothCurve), M.IsCausalTripSegment t p q c

def Physicslib4.Spacetime.IsCausalTrip (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

A causal trip from p to q: a curve which is piecewise a future-oriented causal geodesic, i.e. a finite chain of causal trip segments. Encoded as the transitive closure of single-segment causal precedence.

Equations

• M.IsCausalTrip t p q = Relation.TransGen (M.CausalSegmentPrecedes t) p q

def Physicslib4.Spacetime.CausallyPrecedes (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Prop

Causal precedence: p ≺ q iff there exists a causal trip from p to q, relative to a fixed time orientation.

Equations

• M.CausallyPrecedes t p q = M.IsCausalTrip t p q

def Physicslib4.Spacetime.«term_≺[_,_]_» : Lean.TrailingParserDescr

Causal precedence: p ≺ q iff there exists a causal trip from p to q, relative to a fixed time orientation.

Equations

• One or more equations did not get rendered due to their size.

Chronological and causal futures and pasts

def Physicslib4.Spacetime.chronologicalFuture (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : Set M.Carrier

The chronological future I^+(p) of a point p.

Equations

• M.chronologicalFuture t p = {q : M.Carrier | M.ChronologicallyPrecedes t p q}

def Physicslib4.Spacetime.chronologicalPast (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : Set M.Carrier

The chronological past I^-(p) of a point p.

Equations

• M.chronologicalPast t p = {q : M.Carrier | M.ChronologicallyPrecedes t q p}

def Physicslib4.Spacetime.chronologicalFutureSet (M : Spacetime) (t : M.TimeOrientation) (S : Set M.Carrier) : Set M.Carrier

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

def Physicslib4.Spacetime.chronologicalPastSet (M : Spacetime) (t : M.TimeOrientation) (S : Set M.Carrier) : Set M.Carrier

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

def Physicslib4.Spacetime.causalFuture (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : Set M.Carrier

The causal future J^+(p) of a point p.

Equations

• M.causalFuture t p = {q : M.Carrier | M.CausallyPrecedes t p q}

def Physicslib4.Spacetime.causalPast (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : Set M.Carrier

The causal past J^-(p) of a point p.

Equations

• M.causalPast t p = {q : M.Carrier | M.CausallyPrecedes t q p}

def Physicslib4.Spacetime.causalFutureSet (M : Spacetime) (t : M.TimeOrientation) (S : Set M.Carrier) : Set M.Carrier

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

def Physicslib4.Spacetime.causalPastSet (M : Spacetime) (t : M.TimeOrientation) (S : Set M.Carrier) : Set M.Carrier

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

Spacelike relatedness

def Physicslib4.Spacetime.IsSpacelikeRelated (M : Spacetime) (t : M.TimeOrientation) (p₁ p₂ : M.Carrier) : Prop

Two points p₁, p₂ of a spacetime are spacelike related if p₂ ∉ J^+(p₁) ∪ J^-(p₁).

Equations

• M.IsSpacelikeRelated t p₁ p₂ = (p₂ ∉ M.causalFuture t p₁ ∪ M.causalPast t p₁)

def Physicslib4.Spacetime.IsCompletelySpacelike (M : Spacetime) (t : M.TimeOrientation) (O₁ O₂ : Set M.Carrier) : Prop

Two subsets O₁, O₂ of a spacetime are completely spacelike with respect to each other if every point of O₁ is spacelike related to every point of O₂.

Equations

• M.IsCompletelySpacelike t O₁ O₂ = ∀ p₁ ∈ O₁, ∀ p₂ ∈ O₂, M.IsSpacelikeRelated t p₁ p₂

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.

theorem Physicslib4.Spacetime.isCausal_of_isTimelike (M : Spacetime) {μ : M.SmoothPath} (h : SmoothPath.IsTimelike M μ) : SmoothPath.IsCausal M μ

A timelike path is causal.

theorem Physicslib4.Spacetime.isCausalTripSegment_of_isTripSegment (M : Spacetime) (t : M.TimeOrientation) {p q : M.Carrier} {c : M.SmoothCurve} (h : M.IsTripSegment t p q c) : M.IsCausalTripSegment t p q c

Every trip segment is a causal trip segment.

theorem Physicslib4.Spacetime.causalSegmentPrecedes_of_segmentPrecedes (M : Spacetime) (t : M.TimeOrientation) {p q : M.Carrier} (h : M.SegmentPrecedes t p q) : M.CausalSegmentPrecedes t p q

Single-segment chronological precedence implies single-segment causal precedence.

theorem Physicslib4.Spacetime.chronologicallyPrecedes_trans (M : Spacetime) (t : M.TimeOrientation) {p q r : M.Carrier} (h₁ : M.ChronologicallyPrecedes t p q) (h₂ : M.ChronologicallyPrecedes t q r) : M.ChronologicallyPrecedes t p r

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.

theorem Physicslib4.Spacetime.causallyPrecedes_trans (M : Spacetime) (t : M.TimeOrientation) {p q r : M.Carrier} (h₁ : M.CausallyPrecedes t p q) (h₂ : M.CausallyPrecedes t q r) : M.CausallyPrecedes t p r

Transitivity of causal precedence. p ≺ q and q ≺ r give p ≺ r.

theorem Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes (M : Spacetime) (t : M.TimeOrientation) {p q : M.Carrier} (h : M.ChronologicallyPrecedes t p q) : M.CausallyPrecedes t p q

Chronological precedence implies causal precedence.

theorem Physicslib4.Spacetime.chronologicalFuture_subset_causalFuture (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : M.chronologicalFuture t p ⊆ M.causalFuture t p

The chronological future is contained in the causal future.

theorem Physicslib4.Spacetime.chronologicalPast_subset_causalPast (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) : M.chronologicalPast t p ⊆ M.causalPast t p

The chronological past is contained in the causal past.

Causal-order refinements under the causality condition

def Physicslib4.Spacetime.NoClosedCausalCurve (M : Spacetime) (t : M.TimeOrientation) : Prop

The causality condition (no closed causal curve). A spacetime satisfies the causality condition when no point causally precedes itself: a closed causal curve through p is exactly a causal trip p ≺ p, so its absence is ¬ (p ≺ p) for all p. This is strictly weaker than strong causality and strictly stronger than the chronology condition ¬ (p ≪ p).

Equations

• M.NoClosedCausalCurve t = ∀ (p : M.Carrier), ¬M.CausallyPrecedes t p p

theorem Physicslib4.Spacetime.chronologicallyPrecedes_irrefl (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t) (p : M.Carrier) : ¬M.ChronologicallyPrecedes t p p

Under the causality condition, chronological precedence is irreflexive: ¬ (p ≪ p), because p ≪ p would give the forbidden p ≺ p.

theorem Physicslib4.Spacetime.causallyPrecedes_asymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t) {p q : M.Carrier} (hpq : M.CausallyPrecedes t p q) : ¬M.CausallyPrecedes t q p

Under the causality condition, causal precedence is asymmetric: p ≺ q → ¬ (q ≺ p), since transitivity would otherwise give the forbidden p ≺ p.

theorem Physicslib4.Spacetime.causallyPrecedes_antisymm (M : Spacetime) (t : M.TimeOrientation) (hc : M.NoClosedCausalCurve t) {p q : M.Carrier} (hpq : M.CausallyPrecedes t p q) (hqp : M.CausallyPrecedes t q p) : p = q

Under the causality condition, causal precedence is antisymmetric: p ≺ q → q ≺ p → p = q (in fact both cannot hold, since transitivity gives the forbidden p ≺ p). Thus ≺ is a strict partial order.

Symmetry of spacelike relatedness

theorem Physicslib4.Spacetime.isSpacelikeRelated_comm (M : Spacetime) (t : M.TimeOrientation) {p₁ p₂ : M.Carrier} : M.IsSpacelikeRelated t p₁ p₂ ↔ M.IsSpacelikeRelated t p₂ p₁

Spacelike relatedness is symmetric.

theorem Physicslib4.Spacetime.isCompletelySpacelike_comm (M : Spacetime) (t : M.TimeOrientation) {O₁ O₂ : Set M.Carrier} : M.IsCompletelySpacelike t O₁ O₂ ↔ M.IsCompletelySpacelike t O₂ O₁

Complete spacelike separation is symmetric in its two regions.

theorem Physicslib4.Spacetime.isCompletelySpacelike_mono (M : Spacetime) (t : M.TimeOrientation) {O₁ O₁' O₂ O₂' : Set M.Carrier} (h₁ : O₁' ⊆ O₁) (h₂ : O₂' ⊆ O₂) (h : M.IsCompletelySpacelike t O₁ O₂) : M.IsCompletelySpacelike t O₁' O₂'

Complete spacelike separation is monotone under shrinking either region.

@[simp]

theorem Physicslib4.Spacetime.isCompletelySpacelike_empty_left (M : Spacetime) (t : M.TimeOrientation) (O : Set M.Carrier) : M.IsCompletelySpacelike t ∅ O

The empty region is completely spacelike to anything (on the left).

@[simp]

theorem Physicslib4.Spacetime.isCompletelySpacelike_empty_right (M : Spacetime) (t : M.TimeOrientation) (O : Set M.Carrier) : M.IsCompletelySpacelike t O ∅

The empty region is completely spacelike to anything (on the right).

theorem Physicslib4.Spacetime.isCompletelySpacelike_union_left (M : Spacetime) (t : M.TimeOrientation) (O₁ O₁' O₂ : Set M.Carrier) : M.IsCompletelySpacelike t (O₁ ∪ O₁') O₂ ↔ M.IsCompletelySpacelike t O₁ O₂ ∧ M.IsCompletelySpacelike t O₁' O₂

A union of regions is completely spacelike to O₂ iff each part is.

theorem Physicslib4.Spacetime.isCompletelySpacelike_union_right (M : Spacetime) (t : M.TimeOrientation) (O₁ O₂ O₂' : Set M.Carrier) : M.IsCompletelySpacelike t O₁ (O₂ ∪ O₂') ↔ M.IsCompletelySpacelike t O₁ O₂ ∧ M.IsCompletelySpacelike t O₁ O₂'

O₁ is completely spacelike to a union iff it is to each part.

Monotonicity of set-valued futures and pasts

theorem Physicslib4.Spacetime.chronologicalFutureSet_mono (M : Spacetime) (t : M.TimeOrientation) {S T : Set M.Carrier} (h : S ⊆ T) : M.chronologicalFutureSet t S ⊆ M.chronologicalFutureSet t T

The set-valued chronological future is monotone.

theorem Physicslib4.Spacetime.chronologicalPastSet_mono (M : Spacetime) (t : M.TimeOrientation) {S T : Set M.Carrier} (h : S ⊆ T) : M.chronologicalPastSet t S ⊆ M.chronologicalPastSet t T

The set-valued chronological past is monotone.

theorem Physicslib4.Spacetime.causalFutureSet_mono (M : Spacetime) (t : M.TimeOrientation) {S T : Set M.Carrier} (h : S ⊆ T) : M.causalFutureSet t S ⊆ M.causalFutureSet t T

The set-valued causal future is monotone.

theorem Physicslib4.Spacetime.causalPastSet_mono (M : Spacetime) (t : M.TimeOrientation) {S T : Set M.Carrier} (h : S ⊆ T) : M.causalPastSet t S ⊆ M.causalPastSet t T

The set-valued causal past is monotone.

Alexandrov topology

def Physicslib4.Spacetime.alexandrovBasis (M : Spacetime) (t : M.TimeOrientation) : Set (Set M.Carrier)

The basis sets generating the Alexandrov topology: all sets of the form I^+(p) ∩ I^-(q) for p, q ∈ M.

Equations

• M.alexandrovBasis t = {U : Set M.Carrier | ∃ (p : M.Carrier) (q : M.Carrier), U = M.chronologicalFuture t p ∩ M.chronologicalPast t q}

@[reducible]

def Physicslib4.Spacetime.alexandrovTopology (M : Spacetime) (t : M.TimeOrientation) : TopologicalSpace M.Carrier

The Alexandrov topology on a spacetime M, with respect to a chosen time orientation t: the topology generated by the basis alexandrovBasis consisting of all intersections of chronological futures and pasts.

Equations

• M.alexandrovTopology t = TopologicalSpace.generateFrom (M.alexandrovBasis t)

theorem Physicslib4.Spacetime.isOpen_alexandrov_of_mem_basis (M : Spacetime) (t : M.TimeOrientation) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) : IsOpen B

Every basis set is open in the Alexandrov topology.

theorem Physicslib4.Spacetime.alexandrov_nbhd_univ_of_no_diamond (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} (hx : ∀ s ∈ M.alexandrovBasis t, x ∉ s) {U : Set M.Carrier} (hU : TopologicalSpace.GenerateOpen (M.alexandrovBasis t) U) (hxU : x ∈ U) : U = Set.univ

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

theorem Physicslib4.Spacetime.isOpen_chronologicalFuture_inter_chronologicalPast (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : IsOpen (M.chronologicalFuture t p ∩ M.chronologicalPast t q)

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.

theorem Physicslib4.Spacetime.isOpen_chronologicalFuture (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) (h : ∀ x ∈ M.chronologicalFuture t p, ∃ (b : M.Carrier), M.ChronologicallyPrecedes t x b) : IsOpen (M.chronologicalFuture t p)

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.

theorem Physicslib4.Spacetime.isOpen_chronologicalPast (M : Spacetime) (t : M.TimeOrientation) (p : M.Carrier) (h : ∀ x ∈ M.chronologicalPast t p, ∃ (a : M.Carrier), M.ChronologicallyPrecedes t a x) : IsOpen (M.chronologicalPast t p)

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.