We prove a machine-checked limit theorem for closed physical theories: if a universe supports physically realizable universal computation, stable macroscopic records, and record-level expression of halting facts, then no total computable law can decide all record-truth on the corresponding diagonal-capable fragment. The result is machine-checked in Lean 4 with zero custom axioms on the diagonal-barrier proof chain cited below. The theorem has two parts: \beginenumerate[label=(\roman*)] \item (Physical Universal Computation implies Diagonal Capability) If a framework's record fragment can encode universal computation and express halting, then it is diagonal-capable in the Arithmetic Self-Reference (ASR) sense. \item (Diagonal Capability implies Incompleteness) By the diagonal barrier (Theorem 5.9, machine-checked via Mathlib's halting undecidability), record-truth on the ASR fragment is not computably decidable. \endenumerate Combining these: in any universe where computers exist and their halting behavior is physically meaningful at the record level, no total computable procedure can decide all record-truth questions on the diagonal-capable fragment. This is a Gödel/Turing-class constraint on the form of closed physical theories, now kernel-verified with the premise "computers exist" rather than "ASR is assumed." This paper isolates the formal theorem itself. It does not assume the full downstream ontological or domain-specific claims of the broader program. Its contribution is a precise, machine-checked barrier theorem: once a universe can stably record computations about computations, algorithmic totality fails at the record-semantic level. Trust boundary. The Lean chain is nems-lean (diagonal barrier via Mathlib halting); the physical antecedent is the "universal computation + halting at records" premise bundle stated in the body. See .