GovernanceCert
plain-language theorem explainer
GovernanceCert is a record asserting that the five enumerated institutions stand in bijective correspondence with the five enumerated failure modes. Institutional analysts would cite the structure when checking that democratic maintenance requires every recognition ratio to remain inside the J-cost band. The definition assembles the claim directly from the two inductive enumerations and the explicit one-to-one mapping function.
Claim. Let $I$ be the set of governance institutions and $F$ the set of failure modes. A certificate $G$ satisfies $|I|=5$, $|F|=5$, and the existence of a bijection $I to F$ realized by the explicit institution-to-failure mapping.
background
The module treats democratic governance as five institutions (executive, legislative, judicial, military, press) whose recognition ratios $r_i$ must all lie near 1. Each institution is paired with one canonical failure mode (authoritarianism, oligarchy, rule-of-men, coup risk, information collapse) that occurs precisely when the corresponding $J(r_i)$ exceeds the threshold $J(phi)$. The upstream mapping function supplies the concrete pairing used by the bijection field.
proof idea
Direct record construction that supplies the two cardinality equalities from the Fintype instances on the inductive types together with the bijectivity fact already proved for the explicit mapping function.
why it matters
The certificate supplies the 5-by-5 bijection required by the downstream governanceCert construction. It thereby completes the E7 institutional-failure block, confirming that the same J-cost threshold governing material failure and phase transitions also governs the five democratic institutions. The construction embeds governance inside the unified forcing chain without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.