governanceFailure_count
plain-language theorem explainer
Enumeration of governance failure modes yields exactly five distinct cases under the configDim = 5 convention. Governance analysts would cite the result to confirm completeness of the failure list before analyzing institutional risks. The proof reduces to a single decide tactic that exploits the Fintype derivation on the inductive type.
Claim. $|S| = 5$ where $S = $ {capture, fragmentation, authoritarian drift, corruption, legitimacy collapse}.
background
The module sets governance failure modes equal to configDim D = 5 and lists five canonical modes that correspond to failures of five canonical institutions. The inductive type GovernanceFailure enumerates them as capture, fragmentation, authoritarianDrift, corruption, legitimacyCollapse and derives DecidableEq, Repr, BEq, Fintype. This supplies the local setting for institutional analysis inside Recognition Science with zero sorry statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality from the derived Fintype instance on GovernanceFailure.
why it matters
The theorem supplies the five_failures field inside the downstream governanceFailureCert definition. It completes the enumeration step for the E7 depth treatment of governance failure modes from configDim. The count parallels the forcing-chain derivation of spatial dimension D = 3, here extended to institutional structures with five modes fixed by the configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.