solutionConceptCount
plain-language theorem explainer
The declaration establishes that exactly five canonical solution concepts exist in game theory when aligned with Recognition Science. Game theorists and economists working on RS-derived equilibria would cite it to confirm the match with configDim D. The proof is a direct decision procedure on the finite inductive enumeration of the five concepts.
Claim. The cardinality of the set of solution concepts is five: $ |{Nash, Subgame Perfect, Correlated, Bayesian Nash, Evolutionarily Stable}| = 5 $.
background
The module identifies five canonical solution concepts whose count equals configDim D. SolutionConcept is the inductive type whose constructors are Nash equilibrium, subgame perfect equilibrium, correlated equilibrium, Bayesian Nash equilibrium, and evolutionarily stable strategy. In RS, equilibria arise when the J-cost vanishes in each player's recognition field; the prisoner's dilemma yields positive social cost while stag hunt drives J to its minimum. The sole upstream result is the inductive definition of SolutionConcept itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive type SolutionConcept, whose five constructors are enumerated by the derived Fintype instance.
why it matters
This theorem supplies the five_concepts field of the downstream GameTheoryDepthCert definition, anchoring the claim that game-theoretic depth equals five in the RS framework. It directly instantiates the module statement that five solution concepts equal configDim D. No open questions or scaffolding are indicated in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.