GovernanceInstitution
plain-language theorem explainer
GovernanceInstitution enumerates the five canonical democratic institutions as an inductive type whose constructors are executive, legislative, judicial, military, and press. Recognition Science modelers of institutional stability cite it when establishing finite cardinality or bijective mappings to failure modes. The declaration is realized directly as an inductive definition that derives decidable equality, representation, and finite-type structure.
Claim. Let $I$ be the set of governance institutions consisting of the five elements executive, legislative, judicial, military, and press.
background
Recognition Science models governance through recognition ratios $r_i$ for each institution, with healthy states satisfying $J(r_i)≈0$ where $J(x)=(x+x^{-1})/2-1$. The module treats five institutions as the configuration dimension $D=5$, previously fixed in the sociology layer, and associates each with a canonical failure mode once $J(r_i)$ exceeds the threshold $J(φ)$. The inductive type supplies the domain on which these ratios and thresholds are later evaluated.
proof idea
The declaration is a direct inductive definition with five constructors and no proof obligations beyond the automatic derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the domain for the structure GovernanceCert, which asserts that the cardinality of institutions equals five, the cardinality of failure modes equals five, and the mapping institutionFailureMode is bijective. It realizes the configDim $D=5$ landmark inside the governance application of the J-cost threshold that governs phase transitions throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.