Causal structure on a spacetime

This file formalises the pointwise causal structure attached to a spacetime, following section 10.2 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.

Modelling notes

Mathlib does not currently package "smooth vector field" as a single named type. 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.smooth_in_charts: by writing the chart-local expression and requiring ContDiffWithinAt.

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 ∈ T_pM is timelike if g|_p(v,v) < 0.

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 ∈ T_pM is spacelike if g|_p(v,v) > 0.

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 ∈ T_pM is null if g|_p(v,v) = 0.

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 on a spacetime M is a smooth, non-vanishing, everywhere-timelike vector field on M.

We unbundle the data as:

• field : ∀ x, T_xM, the pointwise tangent vector;
• nonvanishing: field x ≠ 0 for all x;
• timelike_at: field x is timelike at every x;
• smooth: smoothness of the section in any extended chart, expressed via the chart-local form of the field. This is a genuine Prop field of the structure (a ContDiffWithinAt condition on the chart-local representative), discharged for concrete time orientations — see standardMinkowskiTimeOrientation in Minkowski.lean.

• field (x : M.Carrier) : TangentSpace M.model x

  The underlying tangent vector field.

• nonvanishing (x : M.Carrier) : self.field x ≠ 0

  The field is everywhere non-zero.

• timelike_at (x : M.Carrier) : M.IsTimelike (self.field x)

  The field is timelike at every point.

• smooth (x₀ : M.Carrier) : let e := extChartAt M.model x₀; ContDiffWithinAt ℝ ⊤ (fun (y : SpacetimeModel) => (mfderiv M.model M.model (↑e.symm) y) ((mfderiv M.model M.model (↑e) (↑e.symm y)) (self.field (↑e.symm y)))) e.target (↑e x₀)

  The field is smooth as a section of the tangent bundle. We express this via smoothness of its chart-local representative; see Spacetime.smooth_in_charts for the analogous condition for the metric.

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 timelike tangent vector v is future-pointing with respect to a time orientation t if g|_p(t,v) < 0. The blueprint also extends this notion to null vectors by taking limits of timelike future-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 timelike tangent vector v is past-pointing with respect to a time orientation t if g|_p(t,v) > 0. The blueprint also extends this notion to null vectors by taking limits of timelike 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.