The Internality / Outsourcing Schema: A General Lean Theory of Load-Bearing Tasks

We formalize the core structural pattern underlying many NEMS results: if a task is load-bearing for a system's determinacy and is not internally realizable, then any purported completion depends on outsourced (non-internal) structure. We introduce an abstract SystemTaskInterface and prove the Generic Outsourcing Barrier theorem and the Outsourcing Witness corollary. We then instantiate the schema for the NEMS framework, recovering the trichotomy (categorical, internal selector, or externally selected) as a corollary. We further formalize Fundamentality as Internal Completion (Meta-Principle 2 of Paper 82): a theory is foundational precisely when it is either observationally categorical or supplies an admissible internal selector. All results are machine-checked in Lean 4 in the InternalitySchema library of nems-lean, with zero sorry and zero custom axioms. Trust boundary. Results in InternalitySchema are machine-checked in nems-lean . Instantiation prose for Papers 8, 27, 35 maps informal tasks to the schema; audit declarations in Lean; see .