spatial_cost_positive

formal source

  84  rw [Jcost_eq_sq h_ne]; congr 1 <;> ring
  85
  86/-- The spatial cost is strictly positive for any non-zero displacement. -/
  87theorem spatial_cost_positive (ε : ℝ) (hε : -1 < ε) (hε_ne : ε ≠ 0) :
  88    0 < Jcost (1 + ε) := by
  89  rw [Jcost_near_identity ε hε]
  90  exact div_pos (sq_pos_of_ne_zero hε_ne) (mul_pos (by norm_num : (0:ℝ) < 2) (by linarith))
  91
  92/-- **The spatial metric coefficient** at the identity is 1/2,
  93    giving J''(1) = 2 · (1/2) = 1. -/
  94theorem spatial_metric_at_identity :
  95    (1 : ℝ) / (2 * (1 + 0)) = 1 / 2 := by norm_num
  96
  97/-! ## §3  The Minkowski Metric (Forced, Not Postulated) -/
  98
  99/-- The **Minkowski metric** on RS spacetime.
 100    Index 0 = temporal (octave advance), indices 1,2,3 = spatial (Q₃ axes). -/
 101def η (i j : Fin 4) : ℝ :=
 102  if i ≠ j then 0
 103  else if i.val = 0 then -1
 104  else 1
 105
 106private lemma η_eval (i : Fin 4) : η i i = if i.val = 0 then -1 else 1 := by
 107  simp [η]
 108
 109/-- η₀₀ = −1. -/
 110theorem η_00 : η (0 : Fin 4) (0 : Fin 4) = -1 := by simp [η]
 111
 112/-- η₁₁ = +1. -/
 113theorem η_11 : η (1 : Fin 4) (1 : Fin 4) = 1 := by
 114  show (if (1 : Fin 4) ≠ 1 then (0 : ℝ) else if (1 : Fin 4).val = 0 then -1 else 1) = 1
 115  norm_num
 116
 117/-- η₂₂ = +1. -/