1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Vector
  6. Causality
  7. Basic
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct

Causality of Lorentz vectors

@[expose] public section

Classification of lorentz vectors based on their causal character.

inductive CausalCharacter | timeLike | lightLike | spaceLike deriving DecidableEq

A Lorentz vector p is

    lightLike if ⟪p, p⟫ₘ = 0.

    timeLike if 0 < ⟪p, p⟫ₘ.

    spaceLike if ⟪p, p⟫ₘ < 0. Note that ⟪p, p⟫ₘ is defined in the +--- convention.

def causalCharacter {d : ℕ} (p : Vector d) : CausalCharacter := let v0 := ⟪p, p⟫ₘ if v0 = 0 then CausalCharacter.lightLike else if 0 < v0 then CausalCharacter.timeLike else CausalCharacter.spaceLike

causalCharacter are invariant under an action of the Lorentz group.

All goals completed! 🐙
d:ℕp:Vector dh1:¬(minkowskiProduct p) p = 0h2:(minkowskiProduct p) p = 0 ∨ (minkowskiProduct p) p < 0⊢ (minkowskiProduct p) p < 0 All goals completed! 🐙

The Lorentz vector p and -p have the same causalCharacter

d:ℕp:Vector dh:(minkowskiProduct (-p)) (-p) = (minkowskiProduct p) p⊢ (-p).causalCharacter = p.causalCharacter All goals completed! 🐙

The future light cone of a Lorentz vector p is defined as those vectors q such that

    causalCharacter (q - p) is timeLike and

    (q - p) (Sum.inl 0) is positive.

def interiorFutureLightCone {d : ℕ} (p : Vector d) : Set (Vector d) := {q | causalCharacter (q - p) = .timeLike ∧ 0 < (q - p) (Sum.inl 0)}

The backward light cone of a Lorentz vector p is defined as those vectors q such that

    causalCharacter (q - p) is timeLike and

    (q - p) (Sum.inl 0) is negative.

def interiorPastLightCone {d : ℕ} (p : Vector d) : Set (Vector d) := {q | causalCharacter (q - p) = .timeLike ∧ (q - p) (Sum.inl 0) < 0}

The light cone boundary (null surface) of a spacetime point p.

def lightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d) := {q | causalCharacter (q - p) = .lightLike}

The future light cone boundary (null surface) of a spacetime point p.

def futureLightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d) := {q | causalCharacter (q - p) = .lightLike ∧ 0 ≤ (q - p) (Sum.inl 0)}

The past light cone boundary (null surface) of a spacetime point p.

def pastLightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d) := {q | causalCharacter (q - p) = .lightLike ∧ (q - p) (Sum.inl 0) ≤ 0}

Any point p lies on its own light cone boundary, as p - p = 0 has zero Minkowski norm squared.

lemma self_mem_lightConeBoundary {d : ℕ} (p : Vector d) : p ∈ lightConeBoundary p := d:ℕp:Vector d⊢ p ∈ p.lightConeBoundary All goals completed! 🐙

A proposition which is true if q is in the causal future of event p.

def causallyFollows {d : ℕ} (p q : Vector d) : Prop := q ∈ interiorFutureLightCone p ∨ q ∈ futureLightConeBoundary p

A proposition which is true if q is in the causal past of event p.

def causallyPrecedes {d : ℕ} (p q : Vector d) : Prop := q ∈ interiorPastLightCone p ∨ q ∈ pastLightConeBoundary p

Events p and q are causally related.

def causallyRelated {d : ℕ} (p q : Vector d) : Prop := causallyFollows p q ∨ causallyFollows q p

Events p and q are causally unrelated (spacelike separated).

def causallyUnrelated {d : ℕ} (p q : Vector d) : Prop := causalCharacter (p - q) = CausalCharacter.spaceLike

The causal diamond between events p and q, where p is assumed to causally precede q.

def causalDiamond {d : ℕ} (p q : Vector d) : Set (Vector d) := {r | causallyFollows p r ∧ causallyFollows r q}

In Minkowski spacetime with (+---) signature, we can define future-directed vectors as having positive time components (by convention)

def isFutureDirected {d : ℕ} (v : Vector d) : Prop := 0 < timeComponent v

In Minkowski spacetime with (+---) signature, we can define past-directed vectors as having negative time components (by convention)

def isPastDirected {d : ℕ} (v : Vector d) : Prop := timeComponent v < 0