GameType
plain-language theorem explainer
The enumeration of five canonical game configurations supplies the finite set on which Recognition Science recovers Nash equilibrium as the point of vanishing recognition cost. Economists extending the framework to strategic interaction cite this classification to equate equilibrium with J-cost zero and off-equilibrium states with positive cost. The declaration is a direct inductive type whose Fintype instance is derived automatically, immediately enabling the cardinality result used by the downstream certification structure.
Claim. Define the type of strategic game configurations to consist of the five classes zero-sum, cooperative, non-cooperative, symmetric, and repeated.
background
The module recovers game theory inside Recognition Science by setting Nash equilibrium equal to the minimum of the J-cost function, with off-equilibrium states carrying positive cost. Five canonical game classes are introduced to match configuration dimension D = 5. The J-cost is drawn from the imported Cost module and obeys the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The declaration is an inductive definition with exactly five constructors. The Fintype instance is obtained by automatic derivation, which supplies the decidable equality and finite cardinality structure required by the subsequent cardinality theorem.
why it matters
This enumeration supplies the finite set required by the certification structure that asserts both the count of five and the characterization of Nash equilibrium as J-cost at unity equal to zero. It realizes the module claim that the five classes correspond to configuration dimension D = 5 and that Nash equilibrium coincides with minimum recognition cost. The construction therefore bridges the core forcing chain to its economic applications without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.