GovernanceCriterion
The inductive definition enumerates three binary governance criteria modeled on Arrow's impossibility conditions. A political theorist or sociologist working in the configDim framework cites it to count the criteria that no single institution can satisfy simultaneously when D equals 5. It is introduced as a plain inductive type whose derived Fintype instance immediately yields cardinality 3.
claimLet $C$ be the finite set of governance criteria defined by $C = $ {accountability, effectiveness, legitimacy}, where each element is a binary predicate on institutional performance analogous to the conditions appearing in Arrow's theorem.
background
The Governance Design from ConfigDim module (E7) starts from configDim D = 5 and derives exactly five canonical institutions together with five corresponding failure modes. GovernanceCriterion supplies the three binary criteria whose simultaneous satisfaction is impossible for any single institution, reproducing the Arrow-style obstruction inside the Recognition Science setting. The module imports only Mathlib and contains no upstream RS lemmas; the local claim is that the classical five-institution pattern is forced once D = 5 is fixed.
proof idea
The declaration is an inductive definition with three nullary constructors and an empty proof body. The deriving clause automatically installs DecidableEq, Repr, BEq and Fintype instances; downstream cardinality statements are discharged by the decide tactic on the resulting finite type.
why it matters in Recognition Science
GovernanceCriterion is the source of the three_criteria field inside the GovernanceDesignCert structure and of the criterionCount theorem that asserts Fintype.card = 3. It therefore supplies the numerical anchor for the claim that five institutions are required precisely because three criteria cannot be met by fewer. The definition closes the local E7 loop that links configDim D = 5 to the classical institutional pattern while leaving the general forcing chain (T0-T8) untouched.
scope and limits
- Does not prove that no institution can satisfy all three criteria simultaneously.
- Does not specify any mapping from the five institutions to the three criteria.
- Does not reference the phi-ladder, J-cost, or any T0-T8 forcing step.
- Does not connect to physical constants or mass formulas from the core framework.
formal statement (Lean)
39inductive GovernanceCriterion where
40 | accountability | effectiveness | legitimacy
41 deriving DecidableEq, Repr, BEq, Fintype
42