CanonicalInstitution
plain-language theorem explainer
CanonicalInstitution enumerates the five institutions forced by configDim D=5 in the Recognition Science framework. Governance theorists cite the enumeration when deriving the classical separation of powers from dimensional constraints. The declaration is a direct inductive type with five constructors and an automatic Fintype instance.
Claim. Let $I$ be the finite set of canonical institutions given by $I = $ {executive (enforcement), legislative (rule creation), judicial (rule adjudication), military (external defense), press (information)}.
background
The module Sociology.GovernanceDesignFromConfigDim works in the Recognition Science setting where configDim D=5 forces exactly five institutions and five failure modes. CanonicalInstitution is introduced as the inductive type whose constructors are executive, legislative, judicial, military, and press. The module states that this matches the classical five-institutions structure of stable democratic systems and that no single institution can satisfy all three binary governance criteria at once.
proof idea
The declaration is an inductive definition that lists the five constructors directly. It derives DecidableEq, Repr, BEq, and Fintype from the finite enumeration without further lemmas.
why it matters
CanonicalInstitution supplies the type whose cardinality is asserted by GovernanceDesignCert and proved equal to 5 by institutionCount. It occupies the E7 slot by extending the dimensional forcing (T8 D=3 spatial) to sociological configDim D=5, reproducing the observed five-institution pattern. The parent structure GovernanceDesignCert uses the cardinality to certify uniqueness of fullGovernance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.