gameTheoryCert
plain-language theorem explainer
gameTheoryCert constructs the concrete inhabitant of the GameTheoryCert structure by wiring the five-type count and the two J-cost equilibrium properties. Economists and game theorists working in the Recognition Science setting cite it to obtain a certified derivation of Nash equilibrium from the recognition-cost functional. The definition is a direct record constructor that delegates each field to an upstream lemma or decidable enumeration.
Claim. The structure GameTheoryCert is inhabited by the record whose five_types field equals 5, whose nash_eq field asserts J(1) = 0, and whose off_eq field asserts J(r) > 0 for every r > 0 with r ≠ 1.
background
Recognition Science encodes strategic deviation by the J-cost function J(r), which vanishes exactly at the fixed point r = 1 and is strictly positive elsewhere. The structure GameTheoryCert packages three claims: the set of canonical game types has cardinality 5, Nash equilibrium occurs precisely when J = 0, and any off-equilibrium deviation carries positive cost. The module imports the universal J-equilibrium theorem and the J-cost positivity lemma to realize these claims inside the economics domain.
proof idea
The definition is a one-line structure constructor. It assigns the five_types field to the decidable theorem gameTypeCount, the nash_eq field to nash_equilibrium (which reduces to Jcost_unit0), and the off_eq field to off_equilibrium (which applies Jcost_pos_of_ne_one). No additional tactics or reductions occur.
why it matters
The definition supplies the required inhabitant of GameTheoryCert that is referenced by the master certificate gameTheoryCert in CooperationFromSigma. It thereby embeds the classical Nash theorem inside the Recognition Science framework as the statement that equilibrium coincides with the global minimum of J. The construction directly realizes the five-type configuration space and the J = 0 equilibrium condition stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.