GameTheoryDepthCert
plain-language theorem explainer
GameTheoryDepthCert is a structure that records the cardinality of the SolutionConcept type as exactly 5, matching the five standard game-theoretic equilibria. A researcher tracing the Recognition Science derivation of economic equilibria from the J-functional would cite this to fix the dimension of the solution space. The definition is a direct packaging of the Fintype instance on the enumerated inductive type.
Claim. The structure GameTheoryDepthCert consists of the single assertion that the cardinality of the finite type of solution concepts equals 5, where the solution concepts are the five enumerated types: Nash equilibrium, subgame-perfect equilibrium, correlated equilibrium, Bayesian-Nash equilibrium, and evolutionarily stable strategy.
background
The module formalizes five canonical solution concepts as an inductive type whose constructors are nash, subgamePerfect, correlated, bayesianNash, and evolutionarilyStable, equipped with a Fintype instance. Recognition Science identifies game equilibrium with vanishing J-cost in each player's recognition field, so that mutual defection in the Prisoner's dilemma carries positive social cost while coordination in the Stag hunt drives J to its minimum. The module equates the count of these concepts to the configuration dimension D.
proof idea
This is a structure definition that directly records the cardinality statement supplied by the Fintype derivation on the SolutionConcept inductive type. No lemmas are applied; the declaration simply packages the already-derived fact that the type contains exactly five elements.
why it matters
The structure is instantiated by the downstream gameTheoryDepthCert definition and thereby supplies the concrete value 5 for configDim D in the Recognition Science treatment of game theory. It closes the link between the enumerated solution concepts and the five-dimensional equilibrium space required by the J=0 condition, without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.