totalRung
plain-language theorem explainer
totalRung computes the recognition rung of species j in ecosystem E restricted to live set L. It adds the baseline rung of j to the sum of support contributions only from species remaining in L. Cascade modelers cite this quantity when testing whether removal of one species drops another below the ignition threshold φ^19. The definition is a direct arithmetic sum with no auxiliary computation.
Claim. For an ecosystem $E$ on $n$ species with baseline function $b : Fin n → ℝ$ and support function $s : Fin n → Fin n → ℝ$, a live set $L ⊆ Fin n$, and species index $j$, the total rung equals $b(j) + ∑_{i ∈ L} s(i,j)$.
background
The module treats an ecosystem as a finite recognition graph in which each species carries an intrinsic baseline rung before bond support and receives additive contributions from other species. The live set L selects which species remain active and therefore continue supplying support. The Ecosystem structure requires all baselines positive and all supports nonnegative, which keeps the total rung positive by construction.
proof idea
The definition is a one-line arithmetic expression. It extracts the baseline component of species j and adds the Finset sum of the support function over indices in L. No lemmas or tactics are applied; the expression is used verbatim by downstream bankruptcy predicates.
why it matters
totalRung supplies the numerical value tested by IsBankrupt and proved positive by totalRung_pos. It is referenced inside ExtinctionCascadeCert for recovery-time bounds after deep cascades and inside the antimono theorem. In the Recognition framework it encodes the rung-drop step of the structural cascade theorem on finite species graphs, linking ledger bankruptcy to the phi-ladder ignition threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.