cert_inhabited
plain-language theorem explainer
The declaration shows that a certificate structure for coalition sizes exists in the Recognition Science model of three-dimensional configuration spaces. Researchers applying Riker's minimum winning coalition principle to legislative games would cite this when confirming the predicted sizes of 7 total types and 4 minimum winning types. The proof proceeds by a direct term that constructs the Nonempty instance from the explicit cert witness.
Claim. There exists a certificate $C$ such that the total number of coalition types equals 7, the minimum winning coalition size equals 4, twice the minimum winning coalition size is at most the total plus one, and the minimum winning coalition size is positive.
background
In the CoalitionSizeFromConfigDim module the framework models coalition formation in D-dimensional spaces with D fixed at 3 by the unified forcing chain. The total number of distinct coalition types follows the 2^D - 1 count law and equals 7. The minimum winning coalition size is given by ceil(2^{D-1}) and equals 4. The CoalitionSizeCert structure packages the two equalities together with the inequalities 2 * mwcSize ≤ total + 1 and mwcSize > 0.
proof idea
The proof is a one-line term that inhabits the Nonempty type by supplying the cert witness constructed earlier in the module.
why it matters
This result closes the structural theorem for coalition sizes by confirming the certificate is inhabited, directly supporting the RS prediction of MWC size 4 out of 7 at D=3. It feeds the game-theoretic application of the 2^D - 1 count law. The module doc states the falsifier as any empirical study of three-party systems whose modal MWC size departs from ceil(2^{D-1}) by more than one party unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.