GovernanceFailure
plain-language theorem explainer
The inductive definition enumerates five governance failure modes tied directly to configDim equal to 5. Modelers of institutional stability within the Recognition framework cite it when enumerating breakdowns of the five canonical institutions. The declaration lists the five constructors and derives Fintype automatically, enabling immediate cardinality computation by decide.
Claim. Let $G$ be the set of governance failure modes. Then $G$ is the inductive type generated by the constructors capture, fragmentation, authoritarian drift, corruption, and legitimacy collapse, equipped with decidable equality, representation, boolean equality, and finite type structure.
background
The module sets configDim to 5 and defines the resulting five canonical governance failure modes. These modes represent failures of the five canonical institutions in the Recognition Science model. The inductive declaration supplies the finite enumeration required for downstream cardinality arguments, with no axioms or sorrys present.
proof idea
The declaration is an inductive definition that lists the five constructors explicitly. The Fintype instance is derived from the constructors, allowing the companion theorem to compute the cardinality as 5 via the decide tactic.
why it matters
This supplies the base type for the GovernanceFailureCert structure and the governanceFailure_count theorem asserting cardinality exactly 5. It realizes configDim = 5 for governance analysis, paralleling the spatial dimension D = 3 from the unified forcing chain. The module reports zero sorrys, closing this enumeration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.