Closure Audits for Theories: A No-Free-Bits Calculus for Determinacy and Outsourcing Paper 27 of the NEMS Suite

We develop an abstract closure audit calculus for theories of systems. The calculus formalizes a simple meta-question: when does a theory determine facts from observations alone, and when does it silently outsource determinacy to an implicit chooser? The core construction is an observational semantics \Holds : \World \to \Obs \to \mathrmProp inducing an observational equivalence \ObsEq and a quotient of world-types \WType := \World/\ObsEq. A property of worlds is auditable (in the strongest sense) precisely when it factors through \WType; equivalently, it is invariant under \ObsEq. This yields the central audit theorem: decidability on world-types implies invariance, and its sharp contrapositive: any non-invariant predicate is not decidable from world-types (no free bits). The mathematical existence of selector/quotient presentations is distinct from their internal realizability; the substantive closure question concerns realizability, not mere classification. We then analyze the role of selection. Classically, a selector may be presented as a section of the quotient map \toWType : \World \to \WType; in the mechanized development, selectors are equivalently represented as canonical-representative endomaps on \World (world-selectors). We prove these two presentations are canonically equivalent. Classical choice ensures selectors exist, but closure audits distinguish mere existence from internal (effective/definable) selection. We formalize two principled forms of internal symmetry-breaking: (i) canonicalization (gauge-fixing), a map \canon:\World\to\World that collapses each observational equivalence class to a unique representative, and (ii) effective presentation (bounded cover), where an enumeration of worlds hits every world-type within a known bound, enabling total bounded-search selection without choice. Finally, we provide a bridge to Paper 26: any theory that internalizes a representability condition of the appropriate form induces an instance of the minimal self-reference interface \SRIz, and thus inherits diagonal fixed points (\MFP-1) and diagonal barriers in the relevant scope. The entire development is mechanized in Lean 4 (without custom axioms beyond Lean/mathlib; classical choice is used only where explicitly stated), as the Closure library living alongside SelfReference and NemS in the nems-lean artifact. This overview presents the core NEMS theorem engine and selected applications; stronger domain-specific derivation and ontological syn...