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

institutionFailureMode

show as:
view Lean formalization →

The definition assigns each of the five institutions a unique failure mode tied to its recognition ratio crossing the J(φ) threshold. Governance analysts would cite the mapping when checking the bijective correspondence required for institutional certification in the Recognition Science model. It is realized by exhaustive pattern matching on the inductive GovernanceInstitution type.

claimLet $I$ be the set of institutions with elements executive, legislative, judicial, military, press. Let $F$ be the set of failure modes with elements authoritarianism, oligarchy, rule of men, coup risk, information collapse. The function $f:I→ F$ satisfies $f($executive$)= $authoritarianism$, $f($legislative$)= $oligarchy$, $f($judicial$)= $rule of men$, $f($military$)= $coup risk$, $f($press$)= $information collapse$.

background

The module defines GovernanceInstitution as an inductive type with five constructors and FailureMode as a parallel inductive type with five constructors. Each institution carries a recognition ratio $r_i$ (actual competence over mandated competence). The J-cost of an institution is $J(r_i)$, and failure is declared once $J(r_i)$ exceeds the fixed threshold $J(φ)$ where $φ$ is the self-similar fixed point from the T5–T8 forcing chain. The module states that configDim $D=5$ for these institutions and that the democratic maintenance condition requires all five ratios to remain inside the canonical band simultaneously.

proof idea

The declaration is a direct pattern-matching definition on the inductive type GovernanceInstitution. Each constructor is sent to its corresponding FailureMode constructor with no auxiliary lemmas or tactics invoked.

why it matters in Recognition Science

The definition supplies the explicit function required by the GovernanceCert structure, which records that both sets have cardinality five and that the mapping is bijective. The downstream theorem institution_failure_bijection establishes bijectivity by case analysis on this definition. It completes the E7 governance step that links institutional design to the same J(φ) threshold used for phase transitions throughout the framework.

scope and limits

formal statement (Lean)

  47def institutionFailureMode : GovernanceInstitution → FailureMode
  48  | .executive => .authoritarianism
  49  | .legislative => .oligarchy
  50  | .judicial => .ruleOfMen
  51  | .military => .coupRisk
  52  | .press => .informationCollapse
  53

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.