structure
definition
GovernanceDesignCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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