GovernanceAssignment
plain-language theorem explainer
GovernanceAssignment introduces a record type whose three boolean fields encode accountability, effectiveness, and legitimacy. Researchers modeling institutional design under configDim D = 5 cite it when formalizing the classical five-institution pattern. The declaration is a plain structure definition that also installs DecidableEq, BEq, Repr, and Fintype instances.
Claim. A governance assignment is a triple $(a,e,l)$ with $a,e,l \in \{ \text{true}, \text{false} \}$, where the components stand for accountability, effectiveness, and legitimacy respectively.
background
The module derives five canonical institutions (Executive, Legislative, Judicial, Military, Press) directly from configDim D = 5 and observes that the same dimension forces five institutional failure modes. It further notes that no single institution can satisfy all three binary governance criteria at once, an impossibility analogous to Arrow's theorem.
GovernanceAssignment supplies the concrete type for any assignment of those three criteria. The module states that Lean status is zero sorry and zero axiom.
proof idea
Structure definition that declares the three boolean fields and requests the four derived instances; no tactics or lemmas are applied.
why it matters
The structure is the type of the constant fullGovernance, which constructs the single assignment satisfying all three criteria. It therefore supports the module's central claim that five institutions arise from D = 5 and that the three-criterion conjunction is impossible for any one institution. The construction sits inside the Recognition Science forcing chain at the step where configDim D = 5 is obtained from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.