institutionCount
plain-language theorem explainer
The theorem fixes the cardinality of canonical institutions at five when the configuration dimension equals five. Institutional theorists and political modelers cite it to connect Recognition Science's configDim to the observed five-part structure of stable democracies. The proof is a direct decide computation on the derived Fintype instance of the five-constructor inductive type.
Claim. Let $I$ be the finite set of canonical institutions. Then $|I| = 5$, where the elements are executive, legislative, judicial, military, and press, as forced by configDim $D = 5$.
background
The Governance Design from ConfigDim module treats configDim $D = 5$ as the source of exactly five canonical institutions. These are introduced by the inductive definition CanonicalInstitution with constructors executive (enforcement), legislative (rule creation), judicial (rule adjudication), military (external defense), and press (information). The module states that this matches classical five-institution patterns and that no single institution can meet all three binary governance criteria simultaneously.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The inductive type derives DecidableEq, Repr, BEq, and Fintype, so Lean's decision procedure enumerates the five constructors and returns the cardinality directly.
why it matters
The result populates the five_institutions field of governanceDesignCert and supplies institution_count to governanceCert in InstitutionalFailureFromJCost. It completes the E7 governance step by deriving the classical five-institution list from configDim = 5. The declaration supports the module claim that five failure modes likewise equal D = 5 and closes the bijection between institutions and failure modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.