IndisputableMonolith.Governance.GovernanceFailureModesFromConfigDim
IndisputableMonolith/Governance/GovernanceFailureModesFromConfigDim.lean · 34 lines · 4 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3
4/-!
5# Governance Failure Modes from configDim — E7 Depth
6
7Five canonical governance failure modes (= configDim D = 5):
8 capture, fragmentation, authoritarian drift, corruption, legitimacy collapse.
9
10These correspond to failures of the five canonical institutions.
11
12Lean status: 0 sorry, 0 axiom.
13-/
14
15namespace IndisputableMonolith.Governance.GovernanceFailureModesFromConfigDim
16
17inductive GovernanceFailure where
18 | capture
19 | fragmentation
20 | authoritarianDrift
21 | corruption
22 | legitimacyCollapse
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem governanceFailure_count : Fintype.card GovernanceFailure = 5 := by decide
26
27structure GovernanceFailureCert where
28 five_failures : Fintype.card GovernanceFailure = 5
29
30def governanceFailureCert : GovernanceFailureCert where
31 five_failures := governanceFailure_count
32
33end IndisputableMonolith.Governance.GovernanceFailureModesFromConfigDim
34