mwcSize_pos
plain-language theorem explainer
The theorem establishes that the minimum winning coalition size exceeds zero in the Recognition Science model of coalition formation. Game theorists applying Riker's size principle to three-dimensional configuration spaces would cite this when verifying the MWC count. The proof is a one-line wrapper that rewrites via the explicit equality to 4 and normalizes numerically.
Claim. $0 < 2^{D-1}$ where $D=3$ is the configuration dimension, so the minimum winning coalition size equals 4.
background
The module derives coalition sizes from the $2^D-1$ count law at $D=3$, yielding seven total coalition types. The definition mwcSize := $2^{(configDim-1)}$ gives the minimum winning coalition size as ceil($2^{D-1}$), matching the RS prediction of four players out of seven. This setting follows Riker's size principle for rational formation of minimal sufficient coalitions.
proof idea
The proof is a one-line wrapper that rewrites mwcSize using the upstream equality mwcSize_eq (which unfolds to 4) and applies norm_num to confirm the inequality holds.
why it matters
This result is used directly in the CoalitionSizeCert definition, which packages totalCoalitionTypes_eq, mwcSize_eq, mwcSize_le_half, and mwcSize_pos. It completes the structural claim for the RS prediction of MWC size = ceil($2^{D-1}$) at D=3, consistent with the framework's D=3 spatial dimensions and eight-tick octave. The module falsifier notes any empirical modal MWC size departing from the formula by more than one party unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.