pith. machine review for the scientific record. sign in
structure definition def or abbrev high

GovernanceAssignment

show as:
view Lean formalization →

A structure that packages a governance assignment as a triple of boolean flags for accountability, effectiveness, and legitimacy. Political theorists applying Recognition Science to institutional design under configDim D=5 would cite it when counting admissible governance states. The declaration is a direct structure definition that derives decidable equality and finiteness automatically.

claimA governance assignment is a triple $(a,e,l)in{0,1}^3$ whose components record whether the accountability, effectiveness, and legitimacy criteria are satisfied.

background

The module Governance Design from ConfigDim (E7) states that configDim D=5 forces exactly five canonical institutions: executive, legislative, judicial, military, and press. It further notes that the impossibility of satisfying three binary conditions simultaneously (analogous to Arrow's theorem) applies to governance, and that five institutional failure modes likewise equal D=5. The GovernanceAssignment structure supplies the type whose elements are the admissible combinations of the three criteria.

proof idea

Direct structure definition that introduces three boolean fields and derives DecidableEq, BEq, Repr, and Fintype instances.

why it matters in Recognition Science

The definition supplies the carrier type for the downstream fullGovernance construction that isolates the single assignment satisfying all three criteria. It realizes the E7 step of the Recognition Science chain by extending the configDim D=5 forcing (already obtained from the T0-T8 chain) into the sociological domain. The module records that this matches the classical five-institution pattern observed in stable democracies.

scope and limits

formal statement (Lean)

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.