Epistemic Agency Under Diagonal Constraints: Society as a Verification Protocol, Strict Separations, and the Necessity of Role Diversity Paper 31 of the NEMS Suite

Papers 26–30 established a unified abstract spine for self-reference (Paper 26), closure auditing (Paper 27), reflection as a resource (Paper 28), strength-ordered barrier schemas (Paper 29), and self-trust incompleteness (Paper 30). The present paper turns that spine into a theorem-grade theory of epistemic agency and social verification. First, importing Paper 30, we restate as an agency theorem: no diagonal-capable agent admits a universal total internal self-certifier for any nontrivial extensional claim predicate. Second, we formalize a society as an explicit verification protocol: a finite family of verifiers with soundness-on-coverage guarantees, aggregated by an admissible protocol that does not hallucinate answers where all inputs abstain. In a finite claim domain we prove strict separation theorems: there exist societies and protocols whose certified coverage is strictly larger than that of any individual verifier. We then prove necessity theorems: homogeneous societies cannot strictly improve their certification frontier under admissible protocols, and role diversity (non-identical coverage sets) is necessary for strict improvement. These results are formal statements about coverage, admissible aggregation, and diagonal-capable verification architectures; broader institutional analogies are interpretations, not the theorem statements themselves. We add theorem-grade corollaries for control verification (safety, stability, bounded loss) and for stratified self-awareness and the necessity of social mirrors. Finally, we show why society mitigates but does not abolish diagonal barriers: if the society-plus-protocol is treated as a single diagonal-capable system attempting universal total self-certification, the Paper 30 barrier reappears at the societal level. The development is mechanized in Lean 4 as the EpistemicAgency 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. Coverage, admissibility, and diversity theorems are formal statements about finite claim domains and verification protocols; broader institutional readings are interpretive gloss. Mechanization is nems-lean . See .