Institutions Under Diagonal Constraints: Minimal Role Sets, Robust Audit Protocols, and the Impossibility of Universal Self-Governance Paper 40 of the NEMS Suite

Under diagonal-capable regimes, no single institution can be a universal final judge (total, sound, and complete) for nontrivial claim families; robust governance requires role separation and diversity of verification roles, with provable lower bounds on role diversity. This paper imports the diagonal/self-trust barrier (Papers 29–30) as an institutional no-go: no total internal certifier for nontrivial extensional claims. We define institutions as verification protocols with roles, coverage sets, and admissibility (no hallucination). We prove: (1) No universal final judge: under anti-decider closure and \hFP, no institution can be total+sound+complete on nontrivial claim families. (2) k-role lower bound: under a k-way partition and a role-type constraint (each role's coverage in one region), any protocol achieving full certified coverage needs at least k roles. (3) Diversity necessity: strict robustness improvement under admissible protocols implies at least two non-equivalent roles (generalizing Paper 31). These results are formal statements about coverage, admissible aggregation, and diagonal-capable verification architectures; broader institutional analogies are interpretations, not the theorem statements themselves. (4) Meta-barrier: the institution itself cannot universally self-certify if diagonal-capable. We give an explicit toy witness for the k-role bound. The development is mechanized in Lean 4 as the InstitutionalEpistemics 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. Institutional theorems are formal coverage/admissibility statements on finite instance spaces; real-world governance analogies are interpretive. Mechanization is nems-lean . See .