`GovernanceAssignment`

definition

show as: view math explainer →

module: IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim
domain: Sociology
line: 46 · 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 46.

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

used by

fullGovernance IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim

formal source

  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
  67  five_failure_modes := failureModeCount
  68  three_criteria := criterionCount
  69  unique_full_governance := full_governance_unique
  70
  71end IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim

papers checked against this theorem

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