totalRung_pos
plain-language theorem explainer
Any species in a finite ecosystem has strictly positive total rung, defined as baseline plus summed supports from the live set. Ecologists modeling recognition-driven extinction cascades cite this to guarantee that bankruptcy thresholds lie above zero. The proof is a term-mode reduction that unfolds totalRung, invokes baseline positivity and support non-negativity, then applies linarith.
Claim. $0 < E. baseline(j) + L.sum (fun i => E.support i j)$ for every natural number $n$, every ecosystem $E$ on $n$ species, every live set $L$, and every species $j$.
background
An Ecosystem(n) is a finite recognition graph whose structure records a baseline rung vector (intrinsic to each species) and a support matrix (non-negative contributions from live neighbors). The totalRung of species j under live set L is exactly baseline(j) plus the sum of supports from members of L. The module sets this inside the Recognition Science ecology model where extinction occurs precisely when totalRung drops below the life-ignition threshold Z_life = phi^19.
proof idea
Unfolds the definition of totalRung. Applies the baseline_pos field of E to obtain strict positivity of the baseline term. Applies Finset.sum_nonneg together with the support_nonneg field of E to obtain non-negativity of the summed term. Closes with linarith.
why it matters
Supplies the totalRung_pos field of the ExtinctionCascadeCert structure that certifies the monotone fixed-point cascade operator. It anchors the positivity requirement for the bankruptcy step, ensuring the threshold Z_life = phi^19 is crossed only from positive rungs and linking directly to the phi-ladder and T5 J-uniqueness in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.