institutionCount
The declaration asserts that the finite set of canonical democratic institutions has cardinality exactly five. Governance analysts modeling institutional stability via recognition costs would cite this count when enumerating the five failure modes tied to J-cost thresholds. The proof is a direct decision procedure that computes the cardinality from the derived Fintype instance of the enumerated inductive type.
claimThe finite set of canonical democratic institutions, consisting of the executive, legislative, judicial, military, and press branches, has cardinality five.
background
Recognition Science models governance through recognition ratios r_i for each institution, where healthy states require J(r_i) ≈ 0 and failure occurs when any ratio crosses the J(φ) threshold. The module sets configDim D = 5 and enumerates five canonical institutions, each paired with one canonical failure mode. This count matches the upstream result that the set of CanonicalInstitution also has cardinality five.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the cardinality of the Fintype instance derived from the inductive definition of GovernanceInstitution.
why it matters in Recognition Science
This cardinality populates the governanceCert definition and feeds the governanceDesignCert in the Sociology module. It supplies the institutional count step in the E7 governance failure analysis, linking the five institutions to the five failure modes governed by the same J-cost threshold used for disease and phase transitions. The result supports the democratic maintenance condition that all five recognition ratios remain inside the canonical band simultaneously.
scope and limits
- Does not prove dynamical stability of the institutions under J-cost perturbations.
- Does not derive the specific failure modes from the Recognition Composition Law.
- Does not address cross-institution interactions or higher-dimensional governance.
formal statement (Lean)
38theorem institutionCount : Fintype.card GovernanceInstitution = 5 := by decide
proof body
39