mwcSize_le_half
plain-language theorem explainer
The theorem establishes that the minimum winning coalition size is at most half the total number of coalition types, rounded up. Game theorists citing Riker's size principle in three-dimensional configuration spaces would reference this bound to confirm the predicted coalition counts. The proof is a one-line simplification that substitutes the explicit values four for the minimum winning coalition and seven for the total types.
Claim. $2 mwcSize ≤ totalCoalitionTypes + 1$, where mwcSize denotes the minimum winning coalition size $2^{D-1}$ and totalCoalitionTypes denotes the total number of coalition types $2^D - 1$.
background
In the module on coalition formation from configuration dimension, total coalition types are defined as $2^D - 1$ and minimum winning coalition size as $2^{D-1}$. For the three-dimensional case these evaluate to seven and four respectively, as fixed by the equality lemmas totalCoalitionTypes_eq and mwcSize_eq. The module sets the local theoretical setting as a structural theorem supporting Riker's 1962 size principle, with the RS prediction that rational players form the smallest sufficient coalition in a D=3 space yielding four minimum winning types out of seven total.
proof idea
The proof is a one-line wrapper that applies the equality lemmas mwcSize_eq and totalCoalitionTypes_eq to reduce the target inequality to the numerical statement 8 ≤ 8.
why it matters
This bound is packaged into the CoalitionSizeCert certificate in the same module, which assembles the total equality, mwc equality, this inequality, and positivity. It fills the structural theorem for the $2^D - 1$ count law at D=3, matching the empirical median in three-party systems. The declaration touches the framework landmark of eight-tick octave and D=3 spatial dimensions that forces seven coalition types with minimum winning size four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.