InstitutionalFailureMode
plain-language theorem explainer
InstitutionalFailureMode enumerates five failure modes that arise when a governance system with configuration dimension D equals 5 attempts to satisfy three binary criteria simultaneously. Governance theorists cite the enumeration when modeling institutional collapse risks under Arrow-like impossibility constraints. The definition proceeds by direct inductive listing of the five cases, which automatically equips the type with finite cardinality and decidable equality.
Claim. Let $I$ denote the set of institutional failure modes. Then $I$ consists of the five elements state capture, populism, fragmentation, authoritarianism, and information monopoly, so that $|I| = 5$.
background
The module establishes that five canonical institutions (executive, legislative, judicial, military, press) are forced by configDim D = 5, matching classical democratic structures. No single institution can satisfy all three binary governance criteria at once, by an impossibility result analogous to Arrow's theorem. The module documentation states that the five failure modes equal configDim D = 5.
proof idea
The declaration is an inductive definition that lists the five constructors explicitly. It derives DecidableEq, Repr, BEq, and Fintype from the finite enumeration of cases.
why it matters
This supplies the five failure modes required by the GovernanceDesignCert structure, which also records five institutions, three criteria, and unique full governance. It fills the E7 step where failure modes equal configDim D = 5. The construction extends Recognition Science forcing from physical dimensions (D = 3) to social structures while preserving the same self-similar counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.