failureModeCount
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.