Paper 26 gave the universal diagonal calculus (MFP-1, barrier) ; Paper 27 gave the closure audit calculus and internality; Paper 28 gave stratified representability and the Diagonal Closure Theorem. The present paper formalizes selector strength as a preorder of realizability classes (computable, all functions, with advice, etc. ) and proves the barrier theorem family: under anti-decider closure and a fixed-point principle at a strength level, no total decider exists in that strength for any nontrivial extensional predicate. The barrier theorem is indexed by selector strength and requires anti-decider closure plus the fixed-point premise hFP at that strength. Reflection supplies the fixed-point premise when is diagonally closed; Closure supplies the selector-at-strength vocabulary. We prove monotonicity (stronger strength ⇒ more decidable predicates), give two instances (trivial "all functions, " recovering MFP-2 under a global fixed-point engine; and a template for computable-on- reducible to supplying hFP from Mathlib Partrec or SelfReference Kleene), and map the hierarchy to NEMS IIa/IIb as interpretation. The development is mechanized in Lean 4 as the SelectorStrength library in nems-lean, with zero sorry and no custom axioms. This overview presents the core NEMS theorem engine and selected applications; stronger domain-specific derivation and ontological synthesis claims belong to separate release surfaces with their own premise bundles and formal artifacts. Trust boundary. Barrier theorems are indexed: anti-decider closure and the fixed-point premise hFP at a strength level are explicit hypotheses; monotonicity and template instances are not unconditional "everything is undecidable" slogans. Mechanization is nems-lean. See.
Nova Spivack (Sun,) studied this question.