SolutionConcept
SolutionConcept enumerates the five canonical game-theoretic solution concepts that Recognition Science sets equal to configuration dimension D=5. Game theorists formalizing equilibria as J=0 states in recognition fields cite the enumeration when building depth certificates. The declaration is a direct inductive definition deriving Fintype, which enables immediate cardinality verification in downstream results.
claimThe inductive type of solution concepts consists of five constructors corresponding to Nash equilibrium, subgame-perfect equilibrium, correlated equilibrium, Bayesian-Nash equilibrium, and evolutionarily stable strategy, yielding cardinality 5.
background
The module GameTheoryDepthFromRS embeds game theory inside Recognition Science by equating equilibrium with J=0 in each player's recognition field, where J is the J-cost function. Mutual defection in the prisoner's dilemma produces positive social cost J>0, while coordination in stag hunt drives J to its minimum. The module states that five canonical solution concepts equal configDim D=5 and realizes this claim as an inductive type with zero sorry and zero axiom.
proof idea
The declaration is an inductive type with exactly five constructors that derives the instances DecidableEq, Repr, BEq, and Fintype. Cardinality is obtained downstream by the decide tactic applied to Fintype.card on this type.
why it matters in Recognition Science
SolutionConcept supplies the type required by the structure GameTheoryDepthCert, which asserts Fintype.card SolutionConcept =5, and by the theorem solutionConceptCount. It realizes the module claim that five solution concepts equal configDim D, linking game equilibria to the J=0 condition. The module reports zero axioms, closing this fragment of the RS formalization.
scope and limits
- Does not enumerate solution concepts beyond the five listed constructors.
- Does not prove these five exhaust all equilibria satisfying J=0.
- Does not derive configDim from the T0-T8 forcing chain.
- Does not address continuous strategy spaces or infinite games.
formal statement (Lean)
22inductive SolutionConcept where
23 | nash | subgamePerfect | correlated | bayesianNash | evolutionarilyStable
24 deriving DecidableEq, Repr, BEq, Fintype
25