Causality of Lorentz vectors

inductive Lorentz.Vector.CausalCharacter : Type

Classification of lorentz vectors based on their causal character.

• timeLike : CausalCharacter
• lightLike : CausalCharacter
• spaceLike : CausalCharacter

instance Lorentz.Vector.instDecidableEqCausalCharacter : DecidableEq CausalCharacter

Equations

• Lorentz.Vector.instDecidableEqCausalCharacter x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Lorentz.Vector.causalCharacter {d : ℕ} (p : Vector d) : CausalCharacter

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.

Equations

• p.causalCharacter = if ⟪p, p⟫ₘ = 0 then Lorentz.Vector.CausalCharacter.lightLike else if 0 < ⟪p, p⟫ₘ then Lorentz.Vector.CausalCharacter.timeLike else Lorentz.Vector.CausalCharacter.spaceLike

theorem Lorentz.Vector.causalCharacter_invariant {d : ℕ} (p : Vector d) (Λ : ↑(LorentzGroup d)) : (Λ • p).causalCharacter = p.causalCharacter

causalCharacter are invariant under an action of the Lorentz group.

theorem Lorentz.Vector.spaceLike_iff_norm_sq_neg {d : ℕ} (p : Vector d) : p.causalCharacter = CausalCharacter.spaceLike ↔ ⟪p, p⟫ₘ < 0

theorem Lorentz.Vector.neg_causalCharacter_eq_self {d : ℕ} (p : Vector d) : (-p).causalCharacter = p.causalCharacter

The Lorentz vector p and -p have the same causalCharacter

def Lorentz.Vector.interiorFutureLightCone {d : ℕ} (p : Vector d) : Set (Vector d)

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.

Equations

• p.interiorFutureLightCone = {q : Lorentz.Vector d | (q - p).causalCharacter = Lorentz.Vector.CausalCharacter.timeLike ∧ 0 < Lorentz.Vector.toCoord (q - p) (Sum.inl 0)}

def Lorentz.Vector.interiorPastLightCone {d : ℕ} (p : Vector d) : Set (Vector d)

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.

Equations

• p.interiorPastLightCone = {q : Lorentz.Vector d | (q - p).causalCharacter = Lorentz.Vector.CausalCharacter.timeLike ∧ Lorentz.Vector.toCoord (q - p) (Sum.inl 0) < 0}

def Lorentz.Vector.lightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d)

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

Equations

• p.lightConeBoundary = {q : Lorentz.Vector d | (q - p).causalCharacter = Lorentz.Vector.CausalCharacter.lightLike}

def Lorentz.Vector.futureLightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d)

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

Equations

• p.futureLightConeBoundary = {q : Lorentz.Vector d | (q - p).causalCharacter = Lorentz.Vector.CausalCharacter.lightLike ∧ 0 ≤ Lorentz.Vector.toCoord (q - p) (Sum.inl 0)}

def Lorentz.Vector.pastLightConeBoundary {d : ℕ} (p : Vector d) : Set (Vector d)

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

Equations

• p.pastLightConeBoundary = {q : Lorentz.Vector d | (q - p).causalCharacter = Lorentz.Vector.CausalCharacter.lightLike ∧ Lorentz.Vector.toCoord (q - p) (Sum.inl 0) ≤ 0}

theorem Lorentz.Vector.self_mem_lightConeBoundary {d : ℕ} (p : Vector d) : p ∈ p.lightConeBoundary

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

def Lorentz.Vector.causallyFollows {d : ℕ} (p q : Vector d) : Prop

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

Equations

• p.causallyFollows q = (q ∈ p.interiorFutureLightCone ∨ q ∈ p.futureLightConeBoundary)

def Lorentz.Vector.causallyPrecedes {d : ℕ} (p q : Vector d) : Prop

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

Equations

• p.causallyPrecedes q = (q ∈ p.interiorPastLightCone ∨ q ∈ p.pastLightConeBoundary)

def Lorentz.Vector.causallyRelated {d : ℕ} (p q : Vector d) : Prop

Events p and q are causally related.

Equations

• p.causallyRelated q = (p.causallyFollows q ∨ q.causallyFollows p)

def Lorentz.Vector.causallyUnrelated {d : ℕ} (p q : Vector d) : Prop

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

Equations

• p.causallyUnrelated q = ((p - q).causalCharacter = Lorentz.Vector.CausalCharacter.spaceLike)

def Lorentz.Vector.causalDiamond {d : ℕ} (p q : Vector d) : Set (Vector d)

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

Equations

• p.causalDiamond q = {r : Lorentz.Vector d | p.causallyFollows r ∧ r.causallyFollows q}

def Lorentz.Vector.isFutureDirected {d : ℕ} (v : Vector d) : Prop

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

Equations

• v.isFutureDirected = (0 < v.timeComponent)

def Lorentz.Vector.isPastDirected {d : ℕ} (v : Vector d) : Prop

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

Equations

• v.isPastDirected = (v.timeComponent < 0)