Second Incompleteness for Self-Certifying Learners: No Total Internal Certifier Under Diagonal Capability Paper 30 of the NEMS Suite

Papers 26–29 established the diagonal calculus , closure audits , stratified representability and the Diagonal Closure Theorem , and the selector-strength barrier family . The present paper applies this spine to self-trust in learning systems: we formalize certificates, claims, and internal verifiers, then prove that no total internal self-certifier exists for any nontrivial extensional guarantee predicate when the strength level is anti-decider closed and has a fixed-point premise \hFP (supplied by Reflection when \RepClass is diagonally closed). We state the result as a "second incompleteness for self-certifying learners": self-trust cannot be total when the system has diagonal capability (i.e. the fixed-point premise \hFP is available for the relevant class). The impossibility result concerns universal total internal certification for nontrivial extensional claim families under diagonal capability; stratified and restricted self-certification remain available. We then give a positive result: when \hFP is not supplied (e.g. \RepClass not diagonally closed), total internal verifiers can exist (Stratum 1). A minimal toy (certificate = 0) and a learning-flavored sketch (hypothesis fits finite dataset) instantiate the barrier; the minimal toy also instantiates the positive result when \hFP is not assumed. The development is mechanized in Lean 4 as the Learning library in nems-lean, with zero sorry and no custom axioms. 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. Trust boundary. The self-trust barrier is indexed: it assumes anti-decider closure and the fixed-point premise hFP at the relevant strength; stratified positive results hold only where hFP is not supplied. Mechanization is nems-lean . See .