pith. machine review for the scientific record. sign in

IndisputableMonolith.Governance.GovernanceFailureModesFromConfigDim

IndisputableMonolith/Governance/GovernanceFailureModesFromConfigDim.lean · 34 lines · 4 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   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

source mirrored from github.com/jonwashburn/shape-of-logic