nashEquilibriumCert
plain-language theorem explainer
This definition constructs the NashEquilibriumCert instance for the economics module by populating its five_types field with the cardinality result from nashType_count. Game theorists applying Recognition Science to equilibrium refinements would cite it to confirm that configDim equals five yields exactly five canonical types. The construction is a one-line wrapper that directly assigns the decided cardinality theorem.
Claim. Let NashEquilibriumCert be the structure whose field requires that the finite cardinality of the type of Nash equilibrium refinements equals five. The definition nashEquilibriumCert is the instance in which this field is witnessed by the theorem establishing that the cardinality equals five.
background
The module treats Nash equilibrium refinements as determined by a configuration dimension of five, listing the five canonical types as pure-strategy Nash, mixed-strategy Nash, subgame perfect, trembling-hand perfect, and proper equilibrium. Each successive refinement rules out additional non-credible strategies. NashEquilibriumCert is the structure whose single field is five_types : Fintype.card NashType = 5. The sibling theorem nashType_count proves the equality by the decide tactic. Parallel certificates appear in the Decision and GameTheory modules, each certifying Nash properties via J-cost non-negativity and zero-cost at the canonical profile.
proof idea
The definition is a one-line wrapper that directly assigns the five_types field to the theorem nashType_count. That theorem is proved by the decide tactic, which computes the finite cardinality of NashType as five.
why it matters
This definition supplies the required certificate for the economics module and is referenced by the nashEquilibriumCert definitions in Decision.NashEquilibriumFromJCost and GameTheory.NashEquilibriumFromJCost. It records that exactly five equilibrium refinements arise when configDim equals five, consistent with the framework's use of dimensional parameters to classify structures. It supports the larger claim that Nash stability follows from J-cost minimization without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.