institutionFailureMode
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.