isBankrupt_antimono
plain-language theorem explainer
Bankruptcy of species j is antitone in the live set: if j is bankrupt under larger live set L2 then it remains bankrupt under any smaller live set L1. Ecologists and Recognition Science modelers cite the result to guarantee that cascade closure is inclusion-monotone on finite graphs. The proof unfolds totalRung, invokes the non-negative subset-sum inequality, and finishes by linear arithmetic.
Claim. Let $E$ be a finite ecosystem on $n$ species with baseline rungs and non-negative support values. Let $L_1subseteq L_2$ be live sets and let $j$ be a species. If the total rung of $j$ under $L_2$ is strictly less than the life-ignition threshold $Z_{rm life}$, then the total rung of $j$ under $L_1$ is also strictly less than $Z_{rm life}$.
background
An ecosystem $E$ is a finite directed graph whose vertices carry positive baseline rungs and whose directed edges carry non-negative support values. The total rung of species $j$ under live set $L$ is defined as the baseline of $j$ plus the sum of all supports incoming from members of $L$. Species $j$ is bankrupt under $L$ precisely when this total rung lies below the fixed threshold $Z_{rm life}=phi^{19}$ taken from the phi-ladder in Biology.AbiogenesisFirstCrossing.
proof idea
Unfold the definitions of IsBankrupt and totalRung. Apply the library lemma Finset.sum_le_sum_of_subset_of_nonneg to the subset hypothesis together with the non-negativity of support values. Conclude by linarith on the resulting inequality between the two total-rung expressions.
why it matters
The lemma supplies the monotonicity clause inside ExtinctionCascadeCert and is invoked verbatim by extinction_cascade_one_statement. It therefore closes the structural half of the cascade theorem: the closure operator on finite recognition graphs is inclusion-monotone, exactly as required by the ledger-bankruptcy dynamics of Recognition Science. No open scaffolding remains for this direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.