totalCoalitionTypes_eq
plain-language theorem explainer
The theorem fixes the total number of coalition types at 7 once configuration dimension is set to 3. Game theorists applying Riker's size principle inside the Recognition Science model would cite it to anchor the count of distinct coalitions before deriving minimum winning coalition bounds. The proof is a one-line term that unfolds the two definitions and lets norm_num finish the arithmetic.
Claim. With configuration dimension $D=3$, the total number of coalition types satisfies $2^D-1=7$.
background
In this module configuration dimension is the constant 3, representing the three spatial degrees of freedom in the Recognition Science configuration space. Total coalition types is defined directly as $2$ raised to that dimension minus one. The local setting follows the module's account of Riker's 1962 size principle, which predicts seven total coalition types at $D=3$ and a minimum winning coalition of size 4; upstream the same symbol appears in IntegrationGap as $d+2$ and in the cosmology module as the fixed value 5.
proof idea
The proof is a one-line term that unfolds totalCoalitionTypes and configDim, then applies norm_num to reduce the expression $2^3-1$ to the numeral 7.
why it matters
The equality supplies the total-coalition-types field to the CoalitionSizeCert record, which is then used by mwcSize_le_half and the remaining size theorems. It realizes the $2^D-1$ count law at the framework value $D=3$, linking the game-theoretic construction to the eight-tick octave and the spatial-dimension step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.