failureModeCount
The declaration asserts that the inductive type enumerating institutional failure modes has cardinality exactly five. Governance modelers cite it to confirm the one-to-one correspondence with the five democratic institutions fixed by configDim D = 5. The proof is a one-line decision procedure that computes the Fintype cardinality directly from the inductive constructors.
claimLet $F$ be the inductive type whose constructors are authoritarianism, oligarchy, ruleOfMen, coupRisk, and informationCollapse. Then the cardinality of $F$ equals 5.
background
The module treats governance failure as the point where any institution's recognition ratio $r_i$ crosses the J-cost threshold $J(r_i) > J(φ)$. Five institutions are fixed by the earlier configDim D = 5 result, and each is paired with one canonical failure mode: executive capture, legislative gridlock, judicial politicisation, military overreach, and press censorship. The FailureMode inductive type enumerates these five modes and derives the Fintype instance required for cardinality statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the expression Fintype.card FailureMode.
why it matters in Recognition Science
The result populates the failure_count field inside governanceCert, which in turn supplies the institutional certificate used by downstream sociology and engineering modules. It instantiates the framework's repeated pattern of five-mode enumerations (structural safety, fatigue fracture, governance) that follows from D = 5 and the eight-tick octave structure. No open scaffolding remains in the supplied documentation.
scope and limits
- Does not derive the five modes from the Recognition Composition Law.
- Does not prove that real institutions cannot exhibit additional failure modes.
- Does not connect specific numerical J-cost values to each mode.
- Does not establish the empirical frequency of any listed mode.
Lean usage
def governanceCert : GovernanceCert where institution_count := institutionCount failure_count := failureModeCount bijection := institution_failure_bijectionformal statement (Lean)
44theorem failureModeCount : Fintype.card FailureMode = 5 := by decide
proof body
Term-mode proof.
45
46/-- Each institution has exactly one failure mode. -/