institutionCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the institutions from the J-cost function or forcing chain.
- Does not prove dynamical stability or optimality of the five institutions.
- Does not address governance outside the configDim = 5 assumption.
- Does not establish uniqueness of the bijection to failure modes.
formal statement (Lean)
30theorem institutionCount : Fintype.card CanonicalInstitution = 5 := by decide
proof body
31