failureModeCount
plain-language theorem explainer
The theorem proves that the set of institutional failure modes has cardinality exactly five, matching configDim D = 5 in the governance model. Institutional analysts and systems theorists cite it when confirming complete enumerations of failure modes across parallel domains. The proof is a direct computation of finite type cardinality via the decide tactic on the inductive definition.
Claim. Let $F$ be the finite set of institutional failure modes consisting of state capture, populism, fragmentation, authoritarianism and information monopoly. Then $|F| = 5$.
background
The Governance Design from ConfigDim module (E7) states that configDim D = 5 forces five canonical institutions: executive, legislative, judicial, military and press. It correspondingly enumerates five institutional failure modes and notes that the impossibility of satisfying all three binary governance criteria simultaneously (analogous to Arrow's theorem) precludes any single institution from meeting every criterion. Upstream results supply identical cardinality statements: failureModeCount in StructuralSafetyFromJCost, InstitutionalFailureFromJCost and FatigueFractureMechanicsFromJCost each assert Fintype.card of their FailureMode type equals 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to Fintype.card InstitutionalFailureMode = 5. The inductive type InstitutionalFailureMode derives Fintype and lists exactly five constructors, so decide computes the cardinality and discharges the equality.
why it matters
This supplies the failure_count field to the downstream governanceDesignCert definition. It fills the E7 step asserting that configDim D = 5 forces five failure modes, consistent with the classical five-institution structure. The result mirrors the pattern in engineering, materials and governance modules, reinforcing the Recognition Science claim that dimension fixes the number of failure modes. It touches the open question of how these modes interact under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.