Physical Records Imply Non-Effective Internal Adjudication in Perfectly Self-Contained Universes: A Universality Argument from Record Closure, Choice, and Diagonal Capability

We establish a universality-level consequence of Perfect Self-Containment (PSC) for any candidate "closed" theory of the physical universe. Using the machine-checked NEMS classification spine (No External Model Selection) and a machine-checked bridge to the MFRR adjudication principle (Transputation / PT), we show: = (*), leftmargin=2em (Internal adjudication is forced) If macroscopic records do not uniquely determine a realization (record non-categoricity) and the theory is PSC at the NEMS interface level (PSC bundle), then an internal selector/adjudicator exists as a theorem. (Total effective adjudication is forbidden on diagonal-capable record fragments) If the record fragment is diagonal-capable in the precise Arithmetic Self-Reference (ASR) sense, then record-truth on that fragment is not computably decidable, and therefore no internal adjudicator can be total-effective on that fragment. The formal core (classification, bridge forcing, diagonal barrier, and PT non-effectiveness) is kernel-verified in Lean 4 with zero custom axioms, reducing the diagonal constraint to Mathlib's machine-checked halting undecidability theorem. The present paper supplies the remaining physical component: an explicit, conservative argument that our universe satisfies the required premises in any realistic macroscopic-record description, because (a) physical systems implement universal computation and therefore yield diagonal capability at the record level, and (b) physically admissible dynamics generically exhibit record-level underdetermination (genuine choice) in any account that permits stable macroscopic records. Here "given physical universal computation and halting-expressibility at the record level" is the exact formal trigger for the physical incompleteness result. Consequently, any PSC description of our universe must incorporate an internal adjudication principle that cannot be a total computable rule on the diagonal-capable record fragment. This constitutes a Gödel/Turing-class constraint on the form of closed physical theories. 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. The Lean-verified core is Paper 8 via nems-lean ; this paper's universality claim turns on conservative physical premises (record. . .