Physicslib4.Spacetime.CausalStructure

Causal structure on a spacetime

This file formalises the pointwise causal structure attached to a spacetime, following section 10.5 of the AQFT-in-Lean blueprint.

Main definitions

• Physicslib4.Spacetime.IsTimelike, IsSpacelike, IsNull: classification of tangent vectors by the sign of g x v v.
• Physicslib4.Spacetime.TimeOrientation: a smooth non-vanishing global timelike vector field, presented as a section of the tangent bundle.
• Physicslib4.Spacetime.IsTimeOrientable: existence of a time orientation.
• Physicslib4.Spacetime.IsFuturePointing / IsPastPointing: the classification of timelike (and null, by a limit construction) tangent vectors against a chosen time orientation.

Supporting lemmas

• isTimelike_smul_iff, isNull_smul_iff, isSpacelike_smul_iff: scaling-invariance of the three causal classes under nonzero real multiples of a tangent vector.

Modelling notes

Mathlib has no single named type for smooth vector fields. We use the obvious unbundled form: a function t : ∀ x, TangentSpace M.model x together with two pointwise predicates (non-vanishing and timelike) and an unbundled smoothness statement carried as a Prop field. Smoothness of a section of the tangent bundle is captured exactly as in Spacetime.contMDiff: in Mathlib's bundle-section idiom, as ContMDiff of x ↦ TotalSpace.mk' _ x (t x) into the tangent bundle. This is the left-hand side of Bundle.contMDiffAt_section and the shape ContMDiff.mpullback_vectorField expects.

For the null future/past-pointing case we follow the blueprint and define future-pointing null vectors as the closure (in the obvious tangent space topology coming from TangentSpace M.model x ≃ ℝ⁴) of the set of future-pointing timelike vectors. We capture this with the existence of a sequence of future-pointing timelike vectors tending to n. The underlying topology on each tangent space is inherited from Mathlib's tangent space typeclass instances.

Classification of tangent vectors

def Physicslib4.Spacetime.IsTimelike (M : Spacetime) {x : M.Carrier} (v : TangentSpace M.model x) : Prop

A tangent vector v at a point x is timelike when g_x(v, v) < 0.

With the signature (-, +, +, +), timelike vectors are the velocities of massive particles.

Blueprint: def:timelike-spacelike-null-vectors

Equations

• M.IsTimelike v = (((M.val x) v) v < 0)

def Physicslib4.Spacetime.IsSpacelike (M : Spacetime) {x : M.Carrier} (v : TangentSpace M.model x) : Prop

A tangent vector v at a point x is spacelike when g_x(v, v) > 0.

Blueprint: def:timelike-spacelike-null-vectors

Equations

• M.IsSpacelike v = (0 < ((M.val x) v) v)

def Physicslib4.Spacetime.IsNull (M : Spacetime) {x : M.Carrier} (v : TangentSpace M.model x) : Prop

A tangent vector v at a point x is null when g_x(v, v) = 0.

Every tangent vector is exactly one of timelike, null and spacelike (isTimelike_or_isNull_or_isSpacelike). The zero vector is null (isNull_zero); smooth paths have a non-vanishing velocity (SmoothPath), so a null curve moves along the light cone.

Blueprint: def:timelike-spacelike-null-vectors

Equations

• M.IsNull v = (((M.val x) v) v = 0)

Basic classification lemmas

Every tangent vector falls into exactly one of the three classes, fixed by the sign of g|_p(v,v).

theorem Physicslib4.Spacetime.isTimelike_or_isNull_or_isSpacelike (M : Spacetime) {x : M.Carrier} (v : TangentSpace M.model x) : M.IsTimelike v ∨ M.IsNull v ∨ M.IsSpacelike v

Causal trichotomy: every tangent vector is timelike, null, or spacelike.

theorem Physicslib4.Spacetime.not_isSpacelike_of_isTimelike (M : Spacetime) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsTimelike v) : ¬M.IsSpacelike v

A timelike vector is not spacelike.

theorem Physicslib4.Spacetime.not_isTimelike_of_isSpacelike (M : Spacetime) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsSpacelike v) : ¬M.IsTimelike v

A spacelike vector is not timelike.

theorem Physicslib4.Spacetime.not_isNull_of_isTimelike (M : Spacetime) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsTimelike v) : ¬M.IsNull v

A timelike vector is not null.

theorem Physicslib4.Spacetime.not_isNull_of_isSpacelike (M : Spacetime) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsSpacelike v) : ¬M.IsNull v

A spacelike vector is not null.

theorem Physicslib4.Spacetime.isNull_zero (M : Spacetime) {x : M.Carrier} : M.IsNull 0

The zero tangent vector is null.

Scaling invariance of the causal classification

The causal type of a tangent vector depends only on the sign of g(v,v), which scales quadratically under v ↦ c • v. Hence for c ≠ 0 the timelike / null / spacelike classification is invariant under scaling — the algebraic fact behind reparametrisation-invariance of the causal type of a curve.

theorem Physicslib4.Spacetime.val_smul_smul (M : Spacetime) {x : M.Carrier} (c : ℝ) (v : TangentSpace M.model x) : ((M.val x) (c • v)) (c • v) = c ^ 2 * ((M.val x) v) v

The metric square scales quadratically: g(c•v, c•v) = c² · g(v,v).

theorem Physicslib4.Spacetime.isTimelike_smul_iff (M : Spacetime) {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) (v : TangentSpace M.model x) : M.IsTimelike (c • v) ↔ M.IsTimelike v

Scaling invariance of timelikeness. For c ≠ 0, c • v is timelike iff v is.

theorem Physicslib4.Spacetime.isNull_smul_iff (M : Spacetime) {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) (v : TangentSpace M.model x) : M.IsNull (c • v) ↔ M.IsNull v

Scaling invariance of nullness. For c ≠ 0, c • v is null iff v is.

theorem Physicslib4.Spacetime.isSpacelike_smul_iff (M : Spacetime) {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) (v : TangentSpace M.model x) : M.IsSpacelike (c • v) ↔ M.IsSpacelike v

Scaling invariance of spacelikeness. For c ≠ 0, c • v is spacelike iff v is.

Time orientation

structure Physicslib4.Spacetime.TimeOrientation (M : Spacetime) : Type u_1

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

• 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 : M.Carrier) => ⟨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 Physicslib4.Spacetime.IsTimeOrientable (M : Spacetime) : Prop

A spacetime M is time-orientable if it admits a time orientation.

Equations

• M.IsTimeOrientable = Nonempty M.TimeOrientation

Future and past pointing vectors

def Physicslib4.Spacetime.IsFuturePointing (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} (v : TangentSpace M.model x) : Prop

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

Equations

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

def Physicslib4.Spacetime.IsPastPointing (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} (v : TangentSpace M.model x) : Prop

A tangent vector is past-pointing for a time orientation t: timelike with g_x(t(x), v) > 0, or null and a limit of such vectors.

This is the time reverse of Spacetime.IsFuturePointing: v is past-pointing exactly when -v is future-pointing (isPastPointing_iff_isFuturePointing_neg).

Blueprint: def:future-and-past-pointing-vectors

Equations

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

Future/past-pointing classification lemmas

theorem Physicslib4.Spacetime.isTimelike_or_isNull_of_isFuturePointing (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsFuturePointing t v) : M.IsTimelike v ∨ M.IsNull v

A future-pointing vector is either timelike or null.

theorem Physicslib4.Spacetime.isTimelike_or_isNull_of_isPastPointing (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {v : TangentSpace M.model x} (h : M.IsPastPointing t v) : M.IsTimelike v ∨ M.IsNull v

A past-pointing vector is either timelike or null.

theorem Physicslib4.Spacetime.not_isFuturePointing_and_isPastPointing_of_isTimelike (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {v : TangentSpace M.model x} (hv : M.IsTimelike v) : ¬(M.IsFuturePointing t v ∧ M.IsPastPointing t v)

A timelike vector cannot be both future-pointing and past-pointing with respect to a fixed time orientation.

Positive-scaling invariance of orientation

Unlike the causal type (invariant under any non-zero scaling), future/past- pointing is preserved only under scaling by a positive scalar — scaling by a negative one swaps the two. This is the algebraic fact behind the reparametrisation-invariance of the orientation of a curve under orientation-preserving reparametrisations.

theorem Physicslib4.Spacetime.val_field_smul (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} (c : ℝ) (v : TangentSpace M.model x) : ((M.val x) (t.field x)) (c • v) = c * ((M.val x) (t.field x)) v

Linearity of the metric in the second argument: g(t, c • v) = c · g(t, v).

theorem Physicslib4.Spacetime.isFuturePointing_smul_of (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} (hc : 0 < c) {v : TangentSpace M.model x} (h : M.IsFuturePointing t v) : M.IsFuturePointing t (c • v)

Positive scaling preserves future-pointing (forward direction).

theorem Physicslib4.Spacetime.isFuturePointing_smul_iff (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} (hc : 0 < c) (v : TangentSpace M.model x) : M.IsFuturePointing t (c • v) ↔ M.IsFuturePointing t v

Positive-scaling invariance of future-pointing. For c > 0, c • v is future-pointing iff v is.

theorem Physicslib4.Spacetime.isPastPointing_smul_of (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} (hc : 0 < c) {v : TangentSpace M.model x} (h : M.IsPastPointing t v) : M.IsPastPointing t (c • v)

Positive scaling preserves past-pointing (forward direction).

theorem Physicslib4.Spacetime.isPastPointing_smul_iff (M : Spacetime) (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} (hc : 0 < c) (v : TangentSpace M.model x) : M.IsPastPointing t (c • v) ↔ M.IsPastPointing t v

Positive-scaling invariance of past-pointing. For c > 0, c • v is past-pointing iff v is.