GovernanceFailureCert
plain-language theorem explainer
GovernanceFailureCert certifies that the inductive enumeration of governance failure modes has cardinality exactly 5. Researchers modeling institutional stability under configDim = 5 in the Recognition framework cite this structure when fixing the number of canonical modes. The definition supplies a single field that records the Fintype cardinality, with the concrete count supplied by a companion definition in the same module.
Claim. A structure $C$ equipped with a field asserting that the set of governance failure modes has cardinality 5, where the modes are the five enumerated cases capture, fragmentation, authoritarian drift, corruption, and legitimacy collapse.
background
The module defines five canonical governance failure modes tied to configDim D = 5. These modes are capture, fragmentation, authoritarian drift, corruption, and legitimacy collapse, each corresponding to the failure of one of the five canonical institutions. The inductive type GovernanceFailure enumerates exactly these cases and automatically derives Fintype, DecidableEq, and related instances.
proof idea
The declaration is a bare structure definition containing one field of type Prop. No lemmas or tactics are invoked inside the structure itself; the field is populated by the downstream definition governanceFailureCert, which simply assigns the result of the count function to the five_failures field.
why it matters
The structure fixes the governance analysis at exactly five modes, matching the configDim = 5 convention stated in the module header. It is used directly by the definition governanceFailureCert that constructs the concrete certificate instance. Within the Recognition framework this supplies a static enumeration for institutional analysis but does not derive the count from the T0-T8 forcing chain, the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.