Selector Strength and Completion Hierarchies: A Poset of Internal Determinacy, Barriers, and Escape Costs Paper 29 of the NEMS Suite

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 \RepClass 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-\mathbbN 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 .