We present a unified formal calculus of self-reference. From a single stratified interface separating semantic objects from syntactic codes, we prove one master fixed-point theorem and one master diagonal barrier, and recover Gödel's diagonal lemma, Kleene's recursion theorem, Löb-style self-reference, and the NEMS diagonal barrier as instances. The result is a machine-checked unification of major fixed-point and diagonal phenomena that are usually presented separately. The interface has two layers: a minimal layer () whose sole axiom is representability (repr-spec), and a re-entry extension () that additionally requires eval-quote. The Master Fixed-Point Theorem (-1) is the two-sorted mixed form p F (p) ; the Master Diagonal Barrier (-2) rules out total deciders for nontrivial extensional predicates within the representable/internal class (not arbitrary external case-splitters). We prove a Semantic Diagonal Trichotomy via strict separation theorems across Strata 0/1/2, corresponding to NEMS Classes I, IIa, and IIb. Sharp minimality results show each axiom is necessary for its respective theorem—they are not ornamentation, but the precise rebuttal to the charge that the interface is over-engineered. The formalization lives in the SelfReference library of nems-lean; Section records Lean/Mathlib versions and distinguishes the direct NemS. Diagonal barrier route from optional abstract instance encodings (see the honesty note there on instance-route proof status). This overview isolates the calculus; stronger domain-specific and ontological packaging is deliberately left to adjacent papers. Trust boundary. Fixed-point and barrier theorems are conditional on the stratified SRI/CSRI interface and the explicit classical/constructive flags stated in the text; they unify diagonal phenomena in logic, not empirical physics by themselves. Machine-checked artifacts are cited as nems-lean. See.
Nova Spivack (2026) studied this question.