Z_life_gt_one
plain-language theorem explainer
The life ignition threshold exceeds one by construction as the golden ratio to the nineteenth power. Ecologists modeling ledger bankruptcy cascades cite the result to anchor the extinction threshold strictly above the unit rung. The proof reduces directly to the known inequality for phi via unfolding and a power lemma.
Claim. The life-ignition threshold satisfies $1 < phi^{19}$.
background
The module formalizes extinction cascades on finite species graphs where each species has a recognition rung. Extinction occurs when the rung drops below the life-ignition threshold defined as Z_life = phi^19. This threshold comes from the abiogenesis first crossing. Upstream results include one_lt_phi establishing 1 < phi via square root comparisons on the golden ratio. Rung definitions from anchor modules place Z_life at position 19 on the ladder. The setting is a monotone fixed-point iteration for cascade closure on the finite graph.
proof idea
The proof unfolds Z_life to phi^19. It obtains 1 < phi from one_lt_phi. It then applies one_lt_pow₀ with norm_num to reach the conclusion.
why it matters
This supplies the strict inequality needed in ExtinctionCascadeCert to certify threshold positivity and cascade monotonicity. It anchors the Q2 track of Plan v7 by confirming the bankruptcy threshold exceeds unity, consistent with the phi-ladder in the forcing chain T5-T8. The result is used directly by extinctionCascadeCert and ExtinctionCascadeCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.