institutionCount
plain-language theorem explainer
The theorem fixes the cardinality of the canonical governance institutions at five within the Recognition Science model of institutional design. Researchers on democratic structures and J-cost failure modes cite it to anchor the configDim D = 5 count. The proof is a direct computation that enumerates the five constructors of the inductive type using its derived Fintype instance.
Claim. Let GovernanceInstitution be the inductive type whose constructors are executive, legislative, judicial, military, and press. Then the cardinality of this finite type satisfies $ |GovernanceInstitution| = 5 $.
background
The module treats governance as a five-dimensional configuration space whose axes are the recognition ratios r_i of the five institutions. Each ratio measures actual competence against mandated competence; healthy operation requires all r_i near 1 so that J(r_i) stays below the canonical threshold J(φ). The inductive type GovernanceInstitution enumerates exactly these five roles and derives DecidableEq, Repr, BEq, and Fintype. An upstream result in Sociology.GovernanceDesignFromConfigDim establishes the same cardinality for CanonicalInstitution, supplying the dimensional precedent.
proof idea
One-line wrapper that applies the decide tactic. The tactic evaluates the Fintype.card expression by exhaustive enumeration over the five constructors supplied by the inductive definition of GovernanceInstitution.
why it matters
The result populates the institution_count field of governanceCert and is referenced by governanceDesignCert and the parallel institutionCount in Sociology.GovernanceDesignFromConfigDim. It realizes the five-institution structure required by the module's democratic maintenance condition and by the J-cost transition criterion that governs failure modes. The count is consistent with the broader Recognition Science claim that configDim D = 5 governs institutional phase transitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.