theorem
proved
tactic proof
spatial_metric_at_identity
show as:
view Lean formalization →
formal statement (Lean)
94theorem spatial_metric_at_identity :
95 (1 : ℝ) / (2 * (1 + 0)) = 1 / 2 := by norm_num
proof body
Tactic-mode proof.
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
125 norm_num
126
127/-- **η is diagonal**: off-diagonal entries vanish. -/
128theorem η_offdiag (i j : Fin 4) (h : i ≠ j) : η i j = 0 := by
129 simp [η, h]
130
131/-- **η is symmetric**: η(i,j) = η(j,i). -/
132theorem η_symm (i j : Fin 4) : η i j = η j i := by
133 simp only [η]; split_ifs <;> simp_all
134
135/-! ## §4 Metric Signature (1, 3) -/
136
137/-- Each diagonal entry of η is either −1 or +1. -/
138theorem η_diag_values (i : Fin 4) : η i i = -1 ∨ η i i = 1 := by
139 fin_cases i
140 · left; exact η_00
141 · right; exact η_11
142 · right; exact η_22
143 · right; exact η_33
144
145/-- Count of negative diagonal entries = 1 (temporal). -/