Physlib.Relativity.Special.ProperTime

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.SpaceAndTime.SpaceTime.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike

Proper Time

This file introduces 4d Minkowski spacetime.

@[expose] public section

The proper time from q to p. Defaults to zero if p and q have a space-like separation.

def properTime {d : ℕ} (q p : SpaceTime d) : ℝ :=
  √⟪p - q, p - q⟫ₘ

              

lemma properTime_pos_ofTimeLike {d : ℕ} (q p : SpaceTime d)
    (h : causalCharacter (p - q) = .timeLike) :
    0 < properTime q p := byd:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.timeLike⊢ 0 < q.properTime p
  rw [properTimed:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.timeLike⊢ 0 < √((minkowskiProduct (p - q)) (p - q))d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.timeLike⊢ 0 < √((minkowskiProduct (p - q)) (p - q))]d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.timeLike⊢ 0 < √((minkowskiProduct (p - q)) (p - q))
  refine sqrt_pos_of_pos ?_d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.timeLike⊢ 0 < (minkowskiProduct (p - q)) (p - q)
  exact (timeLike_iff_norm_sq_pos (p - q)).mp hAll goals completed! 🐙

lemma properTime_zero_ofLightLike {d : ℕ} (q p : SpaceTime d)
    (h : causalCharacter (p - q) = .lightLike) :
    properTime q p = 0 := byd:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.lightLike⊢ q.properTime p = 0
  rw [properTimed:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.lightLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.lightLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0]d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.lightLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0
  rw [lightLike_iff_norm_sq_zerod:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) = 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0d:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) = 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0] at hd:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) = 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0
  simp only [h, sqrt_zero]All goals completed! 🐙

lemma properTime_zero_ofSpaceLike {d : ℕ} (q p : SpaceTime d)
    (h : causalCharacter (p - q) = .spaceLike) :
    properTime q p = 0 := byd:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.spaceLike⊢ q.properTime p = 0
  rw [properTimed:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.spaceLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.spaceLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0]d:ℕq:SpaceTime dp:SpaceTime dh:causalCharacter (p - q) = CausalCharacter.spaceLike⊢ √((minkowskiProduct (p - q)) (p - q)) = 0
  rw [spaceLike_iff_norm_sq_negd:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) < 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0d:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) < 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0] at hd:ℕq:SpaceTime dp:SpaceTime dh:(minkowskiProduct (p - q)) (p - q) < 0⊢ √((minkowskiProduct (p - q)) (p - q)) = 0
  exact sqrt_eq_zero'.mpr (le_of_lt h)All goals completed! 🐙