CoalitionSizeCert
Recognition Science predicts that three-dimensional configuration spaces yield exactly seven coalition types with a minimum winning coalition of size four. Game theorists citing Riker's size principle in this framework would use the certificate to record the specific equalities and inequalities that follow from the 2^D - 1 count law. The structure is defined directly with the four required fields populated from the dimension-specific computations.
claimA structure requiring that the total number of coalition types equals 7, the minimum winning coalition size equals 4, $2$ times the minimum winning coalition size is at most the total plus one, and the minimum winning coalition size is positive.
background
The module defines totalCoalitionTypes as $2^D - 1$ and mwcSize as $2^{D-1}$ where $D$ is the configuration dimension. The module documentation explains that Recognition Science derives from the $2^D - 1$ Count Law at $D = 3$ the prediction of seven coalition types with a minimum winning coalition of size four, aligning with Riker's Size Principle for rational players forming the smallest sufficient coalition. Upstream definitions supply mwcSize := 2^(configDim - 1) and totalCoalitionTypes := 2^configDim - 1. This local setting specializes the general dimensional framework to three-party legislative systems.
proof idea
The declaration is a structure definition whose four fields record the concrete values totalCoalitionTypes = 7, mwcSize = 4 together with the inequalities 2 * mwcSize ≤ totalCoalitionTypes + 1 and mwcSize > 0. No tactics or lemmas are applied; the structure simply packages these assertions for downstream use.
why it matters in Recognition Science
This structure supplies the certified numerical instance for the coalition size predictions at D = 3. It is used to define the cert instance and to prove cert_inhabited. The module documentation positions it as the structural theorem realizing Riker's (1962) Size Principle within Recognition Science, where the 2^D - 1 count at D = 3 yields the observed median minimum majorities in three-party systems. It closes the link between the configuration dimension and empirical coalition formation data.
scope and limits
- Does not derive the coalition size formulas from the Recognition Composition Law.
- Does not generalize the result beyond D = 3.
- Does not incorporate continuous coalition models or non-discrete player counts.
- Does not validate against specific legislative datasets.
formal statement (Lean)
67structure CoalitionSizeCert where
68 total_eq : totalCoalitionTypes = 7
69 mwc_eq : mwcSize = 4
70 mwc_le_half : 2 * mwcSize ≤ totalCoalitionTypes + 1
71 mwc_pos : 0 < mwcSize
72