pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim

show as:
view Lean formalization →

This module defines configuration dimension as the parameter governing coalition types and minimum winning coalition sizes in Recognition Science game theory. Researchers modeling coalition formation under RS constraints would cite it for the derived equalities and size bounds. It consists of direct definitions and short equality lemmas linking dimension to coalition counts without deeper derivations.

claimLet $d$ denote the configuration dimension. The total number of coalition types is a function of $d$, and the minimum winning coalition size $m$ satisfies $m = m(d)$ with the properties $m(d) > 0$ and $m(d) < d/2$.

background

The module imports the RS time quantum from Constants, where the fundamental tick satisfies tau_0 = 1, and the cost structures from the Cost module that underlie J-cost and defect measures. Configuration dimension serves as the discrete parameter controlling the space of coalitions in this game-theoretic setting. The module introduces total coalition types as the cardinality of possible coalitions, minimum winning coalition size as the smallest subset guaranteeing a win, and a certificate type ensuring the size bounds hold.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the dimensional foundation for coalition analysis in the GameTheory domain, providing inputs for size bounds and certificates that connect to broader RS structures such as the forcing chain and cost functions. It grounds game-theoretic objects in the imported constants and cost definitions, enabling downstream work on coalition formation even though no explicit used-by edges are recorded.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)