timelike_iff_subluminal_velocity

formal source

 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). -/
 299theorem rest_energy_is_mass (m : ℝ) :
 300    m ^ 2 = 0 ^ 2 + 0 ^ 2 + 0 ^ 2 + m ^ 2 := by ring
 301
 302/-- **Massless particles travel at c**: E = |p| when m = 0. -/
 303theorem massless_at_speed_c (E p₁ p₂ p₃ : ℝ)
 304    (h : E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 + 0 ^ 2) :
 305    E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 := by linarith
 306
 307/-- **The minimum rest mass** is the Yang-Mills mass gap Δ = J(φ). -/
 308theorem minimum_rest_mass_is_gap :