deep_cascade_recovery_lower
plain-language theorem explainer
The inequality establishes that recovery time after a 17-step cascade at the mammal Z-rung exceeds phi^16, supplying a lower bound near 2207 natural units that aligns with 10^4-10^5 year mammalian radiation after the K-Pg event under standard tau_0 calibration. Ecologists working with recognition-graph models of ecosystems cite the bound when mapping cascade depth to geological recovery intervals. The argument is a direct algebraic reduction that unfolds the recoveryTime definition and invokes nlinarith on the positivity of phi^16 together with
Claim. $phi^{16} < tau(17)$ where $tau(k) := phi^k$ is the recovery time after a cascade of depth $k$ on the phi-ladder and the index 17 corresponds to the mammal rung.
background
In the extinction-cascade model an ecosystem is a finite recognition graph whose vertices carry rungs Z drawn from the phi-ladder; a species becomes extinct once its rung drops below the ignition threshold Z_life = phi^19. The recoveryTime function is defined by recoveryTime k := phi^k and therefore measures elapsed natural time units tau_0 after a cascade of exact depth k. The upstream lemma one_lt_phi supplies the strict inequality 1 < phi that drives all subsequent comparisons on the ladder.
proof idea
The proof is a one-line wrapper. It unfolds the definition of recoveryTime, rewrites the successor exponent via pow_succ, introduces the two facts 0 < phi^16 and 1 < phi (the latter from one_lt_phi), and closes with nlinarith.
why it matters
The bound is referenced inside the ExtinctionCascadeCert structure that packages the positivity, monotonicity and subset properties required to certify the full cascade closure theorem. It supplies the quantitative link between the abstract phi-ladder iteration and the empirical K-Pg recovery window, consistent with the Recognition Science forcing chain in which phi is the self-similar fixed point. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.