193theorem recoveryTime_strict_mono (k : ℕ) : 194 recoveryTime k < recoveryTime (k + 1) := by
proof body
Term-mode proof.
195 unfold recoveryTime 196 rw [pow_succ] 197 have hk : 0 < phi ^ k := pow_pos phi_pos k 198 have hphi : 1 < phi := one_lt_phi 199 nlinarith 200 201/-- Recovery time at deep cascade (`k = 17`, mammal Z-rung) 202exceeds φ^16 (`≈ 2207`), consistent with `10⁴–10⁵` years for the 203K-Pg mammal radiation under canonical biological τ_0 calibration. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.