pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

InstitutionalFailureMode

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  32inductive InstitutionalFailureMode where
  33  | stateCapture | populism | fragmentation | authoritarianism | informationMonopoly
  34  deriving DecidableEq, Repr, BEq, Fintype
  35

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.