pith. machine review for the scientific record. sign in
def definition def or abbrev high

mwcSize

show as:
view Lean formalization →

Game theorists applying Riker's size principle to recognition science models cite the minimum winning coalition size as two raised to configDim minus one. With the local configuration dimension fixed at three this evaluates to four out of seven total coalition types. The definition is a direct arithmetic expression from the two-to-the-D count law specialized to the minimum winning subset.

claimThe minimum winning coalition size equals $2^{D-1}$ where $D$ is the configuration dimension fixed at three.

background

The game theory module applies Riker's size principle to coalition formation in configuration space. Configuration dimension is defined locally as three, corresponding to three spatial degrees of freedom plus one temporal and one ledger component. Upstream, configDim in IntegrationGap is d plus two while the cosmology variant sets it to five; the local value three specializes the two-to-the-D minus one total coalition types count law. The module states that at D equals three the minimum winning coalition size is four out of seven total types, matching empirical medians in three-party systems.

proof idea

The definition is a direct power expression: two raised to the power of configDim minus one, using the local value of three.

why it matters in Recognition Science

This definition supplies the value four used in CoalitionSizeCert to certify total coalition types equal seven, the size at most half the total plus one, and positivity. It implements the recognition science prediction from the two-to-the-D minus one count law at D equals three spatial dimensions from the forcing chain. The module falsifier is any empirical study of legislative coalition formation where the modal minimum winning size departs from the formula by more than one party unit.

scope and limits

formal statement (Lean)

  53def mwcSize : ℕ := 2 ^ (configDim - 1)

proof body

Definition body.

  54

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.