Closure Without Exhaustion A Theorem of Internal Semantic Non-Exhaustion for Reflexive Systems

No sufficiently expressive reflexive system can contain a final, total, exact internal theory of its own realized semantics. Equivalently: reflexive systems may close over themselves, but they cannot internally exhaust themselves. This is the theorem this paper isolates, states, and places in its proper intellectual context. The theorem sharpens and generalizes classical incompleteness-style barriers. Its target is not merely formal derivability inside arithmetic, but the stronger demand that a realized system fully capture, from within itself, the total semantic truth of its own realized condition. The point is not that self-description is impossible—far from it. Reflexive systems can represent themselves richly, certify wide fragments of their own behavior, and construct stable internal self-models. The theorem is sharper: there is no final internal point at which self-description becomes complete semantic self-exhaustion. Something remains structurally unabsorbed. The paper establishes a clean flagship theorem statement, two independent machine-checked proof routes, an explicit distinction between closure and collapse, a definition of final internal self-theory suitable for broad reuse, a consequence map connecting semantic non-exhaustion to physical incompleteness, non-emulability of execution, observer non-self-exhaustion, and syntax–semantics separation, and a cross-disciplinary argument for why this result deserves primary-theorem status. The theorem is machine-checked in Lean 4 with zero custom axioms. Lean anchor: . nofinalₛelfₜheory. Note on provenance. This theorem is the central summit of a larger machine-checked program (the Reflexive Reality suite) comprising more than one hundred papers and thirteen Lean 4 libraries, all with zero custom axioms and zero sorry on primary theorem chains. The program context is described in the introduction; companion papers are cited in the references. This paper is self-contained.