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

fullGovernance

show as:
view Lean formalization →

fullGovernance constructs the single assignment in which accountability, effectiveness, and legitimacy are simultaneously true. Researchers modeling institutional stability under configDim D=5 cite it when establishing uniqueness of full governance. The definition is realized by a direct structure constructor with no lemmas or reductions.

claimThe full governance assignment is the element of the structure with Boolean fields accountability, effectiveness, and legitimacy all equal to true.

background

GovernanceAssignment is the structure whose three fields are the Boolean predicates accountability, effectiveness, and legitimacy. The module states that configDim D=5 forces exactly five canonical institutions (executive, legislative, judicial, military, press) and that no single institution can satisfy all three binary criteria simultaneously, analogous to Arrow's theorem. Upstream results supply the dimensional pattern: seven plot families, eight kinship systems, seven musical modes, and seven ore classes, each realizing a list whose cardinality matches a Recognition Science dimension.

proof idea

The definition is a one-line constructor application that supplies the triple of true values to the three fields of GovernanceAssignment.

why it matters in Recognition Science

This definition supplies the concrete witness required by the uniqueness theorem full_governance_unique and by the certification structure GovernanceDesignCert. It marks the sole point of three-criterion satisfaction inside the governance model derived from configDim D=5. The construction closes the local instance of the broader forcing pattern already visible in the upstream all-lists from narrative geodesics, kinship cohomology, modal preference, and asteroid spectroscopy.

scope and limits

formal statement (Lean)

  53def fullGovernance : GovernanceAssignment := ⟨true, true, true⟩

proof body

Definition body.

  54
  55/-- Only 1 assignment satisfies all three criteria. -/

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.