equal_displacement_is_lightlike

formal source

 236  norm_num; exact sq_pos_of_ne_zero hx
 237
 238/-- A null displacement (|Δx| = |Δt|) is lightlike. -/
 239theorem equal_displacement_is_lightlike (a : ℝ) :
 240    interval (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) = 0 := by
 241  rw [interval_eq_spatial_minus_temporal]
 242  show (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (1 : Fin 4) ^ 2 +
 243       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (2 : Fin 4) ^ 2 +
 244       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (3 : Fin 4) ^ 2 -
 245       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (0 : Fin 4) ^ 2 = 0
 246  norm_num
 247
 248/-! ## §7  Proper Time and the Lorentz Factor -/
 249
 250/-- **Proper time squared**: τ² = −ds² = (Δt)² − |Δx|². -/
 251def proper_time_sq (v : Displacement) : ℝ := temporal_sq v - spatial_norm_sq v
 252
 253/-- Proper time squared = −interval. -/
 254theorem proper_time_sq_eq_neg_interval (v : Displacement) :
 255    proper_time_sq v = -interval v := by
 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) :