institution_failure_bijection
plain-language theorem explainer
The function assigning each of the five canonical democratic institutions its unique failure mode is bijective. Governance modelers in Recognition Science cite this when confirming that the five institutions stand in one-to-one correspondence with the five canonical failure modes. The proof is a direct term-mode construction that splits bijectivity into injectivity (via exhaustive case analysis and simplification) and surjectivity (via explicit preimage construction for each failure mode).
Claim. The map $f$ from the set of five democratic institutions to the set of five failure modes, given by $f($executive$) =$ authoritarianism, $f($legislative$) =$ oligarchy, $f($judicial$) =$ rule-of-men, $f($military$) =$ coup risk, and $f($press$) =$ information collapse, is bijective.
background
The module treats five democratic institutions whose recognition ratios $r_i$ remain near 1 in healthy states, with failure triggered precisely when $J(r_i)$ exceeds the threshold $J(φ)$. The upstream definition institutionFailureMode supplies the explicit assignment of one failure mode to each institution. This assignment is required to match the configDim $D=5$ already fixed in the sociology layer, ensuring the governance model inherits the same J-cost threshold used for phase transitions elsewhere in the framework.
proof idea
The term proof opens with constructor to separate the two directions of bijectivity. Injectivity follows from case analysis on both input institutions followed by simp_all on the definition of institutionFailureMode. Surjectivity follows from case analysis on the target failure mode, with each case discharged by an exact witness that returns the corresponding institution.
why it matters
The result supplies the bijection field required by the downstream governanceCert definition, which packages institutionCount, failureModeCount, and the bijection into a single certificate. It thereby completes the E7 governance model by confirming that the five-to-five mapping is exact, directly tying institutional failure to the same J-cost threshold that governs disease and ecosystem collapse. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.