1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Vector
  6. Causality
  7. TimeLike
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.Causality.Basic

Properties of time like vectors

@[expose] public section

For timelike vectors with negative time components, their time components multiply to give a positive number

@[simp] lemma timelike_neg_time_component_product {d : ℕ} (v w : Vector d) (hv_neg : v (Sum.inl 0) < 0) (hw_neg : w (Sum.inl 0) < 0) : v (Sum.inl 0) * w (Sum.inl 0) > 0 := d:ℕv:Vector dw:Vector dhv_neg:v (Sum.inl 0) < 0hw_neg:w (Sum.inl 0) < 0⊢ v (Sum.inl 0) * w (Sum.inl 0) > 0 All goals completed! 🐙

For timelike vectors, the Minkowski inner product is positive

lemma timeLike_iff_norm_sq_pos {d : ℕ} (p : Vector d) : causalCharacter p = CausalCharacter.timeLike ↔ 0 < ⟪p, p⟫ₘ := d:ℕp:Vector d⊢ p.causalCharacter = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector d⊢ (if (minkowskiProduct p) p = 0 then CausalCharacter.lightLike else if 0 < (minkowskiProduct p) p then CausalCharacter.timeLike else CausalCharacter.spaceLike) = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝:(minkowskiProduct p) p = 0⊢ CausalCharacter.lightLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) pd:ℕp:Vector dh✝:¬(minkowskiProduct p) p = 0⊢ (if 0 < (minkowskiProduct p) p then CausalCharacter.timeLike else CausalCharacter.spaceLike) = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝:(minkowskiProduct p) p = 0⊢ CausalCharacter.lightLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh:(minkowskiProduct p) p = 0⊢ CausalCharacter.lightLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p All goals completed! 🐙 d:ℕp:Vector dh✝:¬(minkowskiProduct p) p = 0⊢ (if 0 < (minkowskiProduct p) p then CausalCharacter.timeLike else CausalCharacter.spaceLike) = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝¹:¬(minkowskiProduct p) p = 0h✝:0 < (minkowskiProduct p) p⊢ CausalCharacter.timeLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) pd:ℕp:Vector dh✝¹:¬(minkowskiProduct p) p = 0h✝:¬0 < (minkowskiProduct p) p⊢ CausalCharacter.spaceLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝¹:¬(minkowskiProduct p) p = 0h✝:0 < (minkowskiProduct p) p⊢ CausalCharacter.timeLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝:¬(minkowskiProduct p) p = 0h:0 < (minkowskiProduct p) p⊢ CausalCharacter.timeLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p All goals completed! 🐙 d:ℕp:Vector dh✝¹:¬(minkowskiProduct p) p = 0h✝:¬0 < (minkowskiProduct p) p⊢ CausalCharacter.spaceLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p d:ℕp:Vector dh✝:¬(minkowskiProduct p) p = 0h:¬0 < (minkowskiProduct p) p⊢ CausalCharacter.spaceLike = CausalCharacter.timeLike ↔ 0 < (minkowskiProduct p) p All goals completed! 🐙

For timeLike vectors in Minkowski space, the inner product of the spatial part is less than the square of the time component

d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)h_spatial_sum:∑ x, v.spatialPart.ofLp x * v.spatialPart.ofLp x = ∑ i, v (Sum.inr i) * v (Sum.inr i)h_time:v.timeComponent = v (Sum.inl 0)h_norm_pos:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)h:∑ i, v (Sum.inr i) * v (Sum.inr i) < v (Sum.inl 0) * v (Sum.inl 0)⊢ ∑ i, v (Sum.inr i) * v (Sum.inr i) < v (Sum.inl 0) * v (Sum.inl 0) All goals completed! 🐙

For nonzero timelike vectors, the time component is nonzero

d:ℕv:Vector dh:v (Sum.inl 0) = 0hv:∑ i, v (Sum.inr i) * v (Sum.inr i) < 0 * 0⊢ False d:ℕv:Vector dh:v (Sum.inl 0) = 0hv:∑ i, v (Sum.inr i) * v (Sum.inr i) < 0⊢ False d:ℕv:Vector dh:v (Sum.inl 0) = 0hv:∑ i, v (Sum.inr i) * v (Sum.inr i) < 0h_spatial_nonneg:0 ≤ ∑ i, v (Sum.inr i) * v (Sum.inr i)⊢ False All goals completed! 🐙

For timelike vectors, the time component is nonzero

lemma timelike_time_component_ne_zero {d : ℕ} {v : Vector d} (hv : causalCharacter v = .timeLike) : timeComponent v ≠ 0 := time_component_ne_zero_of_timelike hv

A vector is timelike if and only if its time component squared is less than the sum of its spatial components squared

d:ℕv:Vector dh_time_lt_space:⟪v.spatialPart, v.spatialPart⟫_ℝ < v (Sum.inl 0) * v (Sum.inl 0)⊢ 0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) d:ℕv:Vector dh_time_lt_space:⟪v.spatialPart, v.spatialPart⟫_ℝ < v (Sum.inl 0) * v (Sum.inl 0)⊢ ∑ i, v (Sum.inr i) * v (Sum.inr i) < v (Sum.inl 0) * v (Sum.inl 0) All goals completed! 🐙

Time component squared is positive for timelike vectors

@[simp] lemma timeComponent_squared_pos_of_timelike {d : ℕ} {v : Vector d} (hv : causalCharacter v = .timeLike) : 0 < (timeComponent v)^2 := d:ℕv:Vector dhv:v.causalCharacter = CausalCharacter.timeLike⊢ 0 < v.timeComponent ^ 2 All goals completed! 🐙

For timelike vectors, the spatial norm squared is strictly less than the time component squared

d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ < v.timeComponent ^ 2 d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)⊢ ∑ x, ⟪v (Sum.inr x), v (Sum.inr x)⟫_ℝ < v.timeComponent ^ 2 d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)h_time:v.timeComponent = v (Sum.inl 0)⊢ ∑ x, ⟪v (Sum.inr x), v (Sum.inr x)⟫_ℝ < v.timeComponent ^ 2 d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)h_time:v.timeComponent = v (Sum.inl 0)⊢ ∑ x, v (Sum.inr x) * v (Sum.inr x) < v (Sum.inl 0) * v (Sum.inl 0) d:ℕv:Vector dhv:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)h_time:v.timeComponent = v (Sum.inl 0)h_norm_pos:0 < v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i)⊢ ∑ x, v (Sum.inr x) * v (Sum.inr x) < v (Sum.inl 0) * v (Sum.inl 0) All goals completed! 🐙