GameTheoryCert
plain-language theorem explainer
Economists and game theorists working from recognition foundations cite this structure for its certification that exactly five game types exist, with Nash equilibrium at zero J-cost and strictly positive J-cost off equilibrium. It packages the type cardinality, the unit vanishing, and the positivity condition. Each fact is supplied directly by upstream results on J-equilibria and the GameType enumeration.
Claim. A structure asserting that the set of game types has cardinality 5, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every $r>0$ with $r≠1$.
background
In the module deriving game theory from recognition science, the J-cost functional measures recognition cost of strategy profiles, with Nash equilibria identified exactly where this cost reaches its global minimum of zero. The inductive GameType enumerates five canonical forms (zero-sum, cooperative, non-cooperative, symmetric, repeated) whose Fintype cardinality is fixed at five, matching configuration dimension D=5. Upstream, the theorem nash_eq establishes Jcost_unit0, supplying the equilibrium condition Jcost 1 = 0; the positivity statement for r ≠ 1 is stated directly as the off-equilibrium property.
proof idea
This is a structure definition that collects three independent facts: the Fintype cardinality of GameType equals five, the vanishing Jcost 1 = 0 drawn from the nash_eq theorem, and the universal positivity of Jcost away from one. No further proof steps or tactics are applied beyond assembling these components.
why it matters
This certificate realizes the recognition science derivation of Nash equilibrium as the zero of J-cost, feeding directly into the gameTheoryCert definition in the same module and the master GameTheoryCert in CooperationFromSigma. It connects J-uniqueness (T5) and the five-type enumeration to classical game theory, with off-equilibrium positivity ensuring uniqueness of the equilibrium point. It touches the open question of embedding concrete economic models into the abstract RS type system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.