proper_time_from_velocity

formal source

 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)
 290
 291/-! ## §8  Energy-Momentum Relation from J-Cost -/
 292
 293/-- The energy-momentum relation (algebraic identity from the metric). -/
 294theorem energy_momentum_relation (E p₁ p₂ p₃ m : ℝ)
 295    (h : E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 + m ^ 2) :
 296    E ^ 2 - (p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2) = m ^ 2 := by linarith
 297
 298/-- **Rest energy = rest mass** (in natural units c = 1). -/