gamma_ge_one

formal source

  37noncomputable section
  38
  39/-- Lorentz factor γ ≥ 1 always. -/
  40theorem gamma_ge_one (v c : ℝ) (hc : 0 < c) (hv : |v| < c) :
  41    1 ≤ c / Real.sqrt (c^2 - v^2) := by
  42  rw [le_div_iff (Real.sqrt_pos.mpr (by nlinarith [sq_nonneg v, sq_abs v, abs_lt.mp hv]))]
  43  rw [one_mul]
  44  apply Real.le_sqrt.mpr
  45  constructor
  46  · positivity
  47  · nlinarith [sq_abs v, abs_lt.mp hv]
  48
  49/-- J-cost at rapidity: J(cosh θ) = cosh θ - 1 = γ - 1 ≥ 0. -/
  50theorem jcost_cosh_is_gamma_minus_one (theta : ℝ) :
  51    Jcost (Real.cosh theta) = Real.cosh theta - 1 := by
  52  unfold Jcost
  53  have h_cosh_pos : 0 < Real.cosh theta := Real.cosh_pos theta
  54  rw [Real.cosh_inv (Real.cosh theta) h_cosh_pos.ne']
  55  ring
  56
  57/-- Mass-energy: m·c² on the φ-ladder at rung r. -/
  58def mass_energy_RS (r : ℕ) : ℝ := phi ^ r * phi ^ (-(5:ℤ))
  59
  60/-- `mass_energy_RS r > 0`. -/
  61theorem mass_energy_pos (r : ℕ) : 0 < mass_energy_RS r := by
  62  unfold mass_energy_RS
  63  exact mul_pos (pow_pos phi_pos r) (zpow_pos phi_pos (-5))
  64
  65structure SpecialRelativityDeepCert where
  66  jcost_cosh_identity : ∀ θ : ℝ, Jcost (Real.cosh θ) = Real.cosh θ - 1
  67  mass_energy_pos : ∀ r : ℕ, 0 < mass_energy_RS r
  68  structural : True  -- SR follows from J-cost symmetry
  69
  70noncomputable def specialRelativityDeepCert : SpecialRelativityDeepCert where