`failureModeCount`

proved

show as: view math explainer →

module: IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim
domain: Sociology
line: 36 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  33  | stateCapture | populism | fragmentation | authoritarianism | informationMonopoly
  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36theorem failureModeCount : Fintype.card InstitutionalFailureMode = 5 := by decide
  37
  38/-- Three binary governance criteria (analogous to Arrow's conditions). -/
  39inductive GovernanceCriterion where
  40  | accountability | effectiveness | legitimacy
  41  deriving DecidableEq, Repr, BEq, Fintype
  42
  43theorem criterionCount : Fintype.card GovernanceCriterion = 3 := by decide
  44
  45/-- A governance assignment. -/
  46structure GovernanceAssignment where
  47  accountability : Bool
  48  effectiveness : Bool
  49  legitimacy : Bool
  50  deriving DecidableEq, BEq, Repr, Fintype
  51
  52/-- All three criteria = full governance. -/
  53def fullGovernance : GovernanceAssignment := ⟨true, true, true⟩
  54
  55/-- Only 1 assignment satisfies all three criteria. -/
  56theorem full_governance_unique :
  57    (Finset.univ.filter (· = fullGovernance)).card = 1 := by decide
  58
  59structure GovernanceDesignCert where
  60  five_institutions : Fintype.card CanonicalInstitution = 5
  61  five_failure_modes : Fintype.card InstitutionalFailureMode = 5
  62  three_criteria : Fintype.card GovernanceCriterion = 3
  63  unique_full_governance : (Finset.univ.filter (· = fullGovernance)).card = 1
  64
  65def governanceDesignCert : GovernanceDesignCert where
  66  five_institutions := institutionCount

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.