mwcSize_eq
plain-language theorem explainer
The minimum winning coalition size equals four when the configuration dimension is three. Game theorists invoking Riker's size principle in spatial models would cite this equality to fix the coalition threshold from dimension count. The proof is a one-line wrapper that unfolds the definitions of minimum winning coalition size and configuration dimension then normalizes the resulting arithmetic expression.
Claim. In a configuration space of dimension three the minimum winning coalition size equals four.
background
The module derives coalition sizes from the configuration dimension D, where D counts independent spatial degrees of freedom plus ledger balance in a recognition event. Total coalition types are given by 2^D - 1. The minimum winning coalition size follows the formula ceil(2^(D-1)). At D = 3 this yields four out of seven total types, matching the median observed in three-party legislative systems. The local setting is the structural theorem realizing Riker's 1962 size principle inside Recognition Science via the 2^D - 1 count law. Upstream results include the definition of configuration dimension as d + 2 from IntegrationGap and the forcing of D = 3 from the unified forcing chain.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of mwcSize and configDim, then applies norm_num to reduce the equality to a numerical identity that holds by direct computation.
why it matters
This theorem supplies the concrete value mwcSize = 4 that is packaged into the CoalitionSizeCert record together with the total-coalition equality and the half-size bound. It fills the D = 3 case of the RS prediction from the 2^D - 1 count law, consistent with the eight-tick octave and the forcing of three spatial dimensions. The result is used by the sibling theorems mwcSize_le_half and mwcSize_pos and by the certificate construction that certifies the structural claim for Riker's principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.