The Survivor Calculus: A Generic Admissibility Cascade for Theory Spaces

We formalize the admissibility cascade underlying the NEMS cosmological program: candidate theory spaces are progressively filtered by closure-compatibility, survivor-compatibility, and further structured admissibility classes. We introduce an abstract Cascade as a list of constraints on a base space, define residual classes R_k as the sets satisfying the first k constraints, and prove the Monotone Cascade Theorem: R_k+1 \subseteq R_k. This packages the filtering structure of Papers 79–80 into a generic reusable framework. The cascade is machine-checked in Lean 4 in the SurvivorCalculus library of nems-lean, with zero sorry and zero custom axioms. Trust boundary. Monotone cascade lemmas are in nems-lean SurvivorCalculus; cosmological interpretation instantiates Papers 79–80 and is not a separate formal universe claim; see .