Determinism No-Go Under Perfect Self-Containment: Diagonal-Capable Records Forbid Total-Effective Record Determinism in Theories with Genuine Record-Divergent Choice

We prove a determinism no-go theorem for closed physical theories with macroscopic records. Using the machine-checked NEMS classification spine and the machine-checked diagonal barrier, we show that in any perfectly self-contained (PSC) framework that is both (i) diagonal-capable at the record level (i.e. it can encode universal computation and halting as record-truth), and (ii) admits genuine record-divergent choice (multiple admissible continuations disagreeing on records), there is no total effective deterministic law that maps past records to unique future records on the diagonal-capable fragment. Formally, any purported total computable "record determinism" function would induce a total computable decider for diagonal-capable record-truth, contradicting the diagonal barrier (proved via reduction to Mathlib's halting undecidability theorem). The proof is kernel-verified in Lean 4 with zero custom axioms. This establishes a Gödel/Turing-class limitation on deterministic closure: if a theory is PSC and admits record-divergent choice, then any determinism compatible with diagonal-capable records must be non-total-effective (or must retreat to record-categoricity / triviality). Given physical universal computation and halting-expressibility at the record level, determinism is ruled out, not assumed. 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.