We give a stratified certification calculus with nontrivial semantics: CertifiableAt (S, C) means there exists an admissible internal verification protocol (roles, coverage) at strength S that certifies C in the coverage sense: the aggregate verifier is non-abstaining on every instance in C under admissible aggregation. The proof system S mirrors protocol combinators (axiom from role coverage, union, subset, stratum monotonicity). We prove soundness (T50. 1): every derivation yields a protocol witness; completeness (T50. 2): every protocol witness normalizes to a derivation; and maximality (T50. 3): any extension yielding a total decider for an extensional nontrivial predicate on a diagonal-capable domain contradicts the SelectorStrength barrier (Paper 29). Thus the calculus is complete and maximally complete under NEMS constraints. Mechanized in Lean 4 (CertificationLogic) ; 0 custom axioms on the capstone chains. Primary anchors: capstone, capstone, ₘaximality. Trust boundary. Machine-checked claims are conditional on the Lean kernel, toolchain pin, and the nems-lean definitions cited in. Discussion of physics or institutional applications is interpretive and relies on modeling bridges in.
Nova Spivack (Sun,) studied this question.