InstitutionalDesignCert
plain-language theorem explainer
InstitutionalDesignCert defines a structure that embeds a CanonicalCert to certify institutional designs via J-cost on power-distribution ratios. Sociologists applying Recognition Science to governance would cite it when checking that observed power concentration over balanced distribution keeps J-cost inside the canonical band for every institution pair. The declaration is a one-field structure that directly reuses the upstream certificate without added constraints.
Claim. An institutional design certificate is a structure whose sole field is a base canonical certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$.
background
The module develops E7 on institutional design from J-cost on power-distribution ratio. It compounds with Sociology/PoliticalSystemsFromSigmaConservation, where five canonical institutions equal configDim D. For each institution pair the ratio r equals observed power concentration divided by balanced distribution; stable governance requires J-cost to remain below the canonical band on every pair, while institutional capture crosses it.
proof idea
The declaration is a structure definition containing the single field base of type CanonicalCert. It functions as a one-line wrapper that directly embeds the upstream CanonicalCert structure.
why it matters
This structure supplies the certificate type used by the downstream institutionalDesignCert definition in the same module. It bridges the CanonicalCert from CanonicalJBand into sociological modeling, allowing governance stability to be expressed through the J-cost band on power ratios. The construction reuses the six-clause certificate whose phi-band clause (0.11 to 0.13) originates in the J-uniqueness properties of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.