spatial_metric_at_identity

formal source

  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. -/
 118theorem η_22 : η (2 : Fin 4) (2 : Fin 4) = 1 := by
 119  show (if (2 : Fin 4) ≠ 2 then (0 : ℝ) else if (2 : Fin 4).val = 0 then -1 else 1) = 1
 120  norm_num
 121
 122/-- η₃₃ = +1. -/
 123theorem η_33 : η (3 : Fin 4) (3 : Fin 4) = 1 := by
 124  show (if (3 : Fin 4) ≠ 3 then (0 : ℝ) else if (3 : Fin 4).val = 0 then -1 else 1) = 1