gameTheoryDepthCert
plain-language theorem explainer
The declaration supplies a certificate that game theory contains exactly five canonical solution concepts, aligning with the configuration dimension D = 5 asserted in Recognition Science. A researcher linking game-theoretic equilibria to the J-functional would cite this to fix the count of Nash, subgame-perfect, correlated, Bayesian-Nash, and evolutionarily stable concepts. The definition is a one-line wrapper that directly assigns the five_concepts field from the decide-proven cardinality theorem.
Claim. Let SolutionConcept be the finite type enumerating the five canonical solution concepts. The certificate asserts that its cardinality satisfies $|SolutionConcept| = 5$.
background
GameTheoryDepthCert is the structure whose sole field requires Fintype.card SolutionConcept = 5. The module equates this cardinality with configDim D = 5 and notes that equilibria correspond to J = 0 in each player's recognition field, while mutual defection in the Prisoner's dilemma produces positive social cost J > 0 and coordination in the Stag hunt drives J toward its minimum.
proof idea
The definition is a one-line wrapper that populates the five_concepts field of GameTheoryDepthCert by direct reference to the theorem solutionConceptCount, which itself is discharged by the decide tactic on the enumerated type SolutionConcept.
why it matters
This supplies the concrete count of five solution concepts required by the Recognition Science claim that configDim D equals 5. It closes the link between the abstract structure GameTheoryDepthCert and the enumerated list of equilibria types. No downstream uses appear in the current graph, leaving open whether the certificate will be invoked in proofs of equilibrium stability under the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.