energy_momentum_relation

formal source

 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 :
 309    0 < massGap ∧ massGap = (Real.sqrt 5 - 2) / 2 :=
 310  ⟨massGap_pos, rfl⟩
 311
 312/-! ## §9  The Arrow of Time from the Octave -/
 313
 314/-- **SE-009: The arrow of time**. Recognition advances monotonically. -/
 315theorem arrow_of_time :
 316    temporal_dim = 1 ∧ eight_tick = 8 ∧ ∀ t : ℕ, t < t + 1 :=
 317  ⟨rfl, rfl, fun _ => Nat.lt_succ_of_le le_rfl⟩
 318
 319/-! ## §10  Exclusion of Alternative Signatures -/
 320
 321theorem not_euclidean : ¬(temporal_dim = 0) := by simp [temporal_dim]
 322theorem not_split_signature : ¬(temporal_dim = 2) := by simp [temporal_dim]
 323theorem not_three_temporal : ¬(temporal_dim = 3) := by simp [temporal_dim]
 324theorem not_1_2_signature : ¬(spatial_dim = 2) := by simp [spatial_dim, D_physical]