`fullGovernance`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim on GitHub at line 53.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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.