theorem
proved
governanceFailure_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Governance.GovernanceFailureModesFromConfigDim on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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