Necessary Incompleteness of Internal Semantic Self-Description: The Non-Self-Erasure Theorem and Semantic Remainder in Reflexive Systems Paper 51 of the NEMS Suite

Papers 26–30 established a general diagonal calculus, closure audits and no-free-bits, reflection as a graded resource, selector-strength barrier schemas, and self-trust incompleteness for learners. Later papers extended the same barrier architecture to agency, self-awareness, institutions, and certification logics. The present paper isolates a deeper target: internal semantic self-capture at the realized-system level. We define a self-semantic frame: a family of internally encoded claims whose truth is the realized semantic truth of the system itself. We then define final self-theories and prove the flagship theorem: no sufficiently expressive diagonally capable realized system can internally contain a final theory (internal, total, and exact) of its own realized semantics. This rules out internal semantic self-exhaustion. We then introduce two stronger notions. First, weak self-erasure: a final self-theory whose own verdict behavior lies inside the same self-semantic claim family. Second, strong self-erasure: an exact internal semantic image closed under self-application. Both are ruled out as corollaries of the main theorem. Finally, we prove a positive master statement: every internal self-theory either fails totality or leaves an irreducible semantic remainder. This yields a general non-self-erasure principle: reflexive closure does not collapse a system into a pointlike self-identity; the system may return to itself, but cannot fully erase the distinction between itself and its own internal semantic image. A physical corollary states that no closed PSC universe contains a final internal GUT that fully exhausts its own realized semantics. The development is mechanized in Lean 4 as the SemanticSelfDescription library in nems-lean, with zero sorry and no custom axioms in the new modules. Primary Lean anchor: SemanticSelfDescription. nofinalₛelfₜheory (see). Trust boundary. Machine-checked claims are conditional on the kernel, toolchain pin, and the cited. lean sources. Physical and philosophical glosses are interpretive bridges.