proper_time_sq_pos_of_timelike

formal source

 256  simp [proper_time_sq, interval_eq_spatial_minus_temporal]
 257
 258/-- Proper time squared is positive for timelike displacements. -/
 259theorem proper_time_sq_pos_of_timelike (v : Displacement) (h : interval v < 0) :
 260    0 < proper_time_sq v := by
 261  rw [proper_time_sq_eq_neg_interval]; linarith
 262
 263/-- **The velocity parameter**: v² = |Δx|²/(Δt)². -/
 264def velocity_sq (v : Displacement) (_ : v ⟨0, by omega⟩ ≠ 0) : ℝ :=
 265  spatial_norm_sq v / temporal_sq v
 266
 267/-- **Proper time from velocity**: dτ² = (Δt)²(1 − v²). -/
 268theorem proper_time_from_velocity (v : Displacement)
 269    (ht : v ⟨0, by omega⟩ ≠ 0) :
 270    proper_time_sq v = temporal_sq v * (1 - velocity_sq v ht) := by
 271  have h_ne : temporal_sq v ≠ 0 := by unfold temporal_sq; exact pow_ne_zero 2 ht
 272  suffices temporal_sq v * (1 - spatial_norm_sq v / temporal_sq v) =
 273      temporal_sq v - spatial_norm_sq v by
 274    simp only [proper_time_sq, velocity_sq]; linarith
 275  field_simp [h_ne]
 276
 277/-- **Subluminal velocity for timelike**: τ² > 0 iff v² < 1. -/
 278theorem timelike_iff_subluminal_velocity (v : Displacement)
 279    (ht : v ⟨0, by omega⟩ ≠ 0) :
 280    0 < proper_time_sq v ↔ velocity_sq v ht < 1 := by
 281  rw [proper_time_from_velocity v ht]
 282  have h_t_pos : 0 < temporal_sq v := by
 283    unfold temporal_sq; exact sq_pos_of_ne_zero ht
 284  constructor
 285  · intro h
 286    by_contra hle; push_neg at hle
 287    have : 1 - velocity_sq v ht ≤ 0 := by linarith
 288    nlinarith
 289  · intro hv; exact mul_pos h_t_pos (by linarith)