nashEquilibriumCert
plain-language theorem explainer
The definition assembles a certificate that the joint homeostasis state at action ratio r=1 is a Nash equilibrium under J-cost minimization in symmetric games. Game theorists and decision theorists in the Recognition Science framework cite it to connect zero-cost recognition to equilibrium stability. The construction is a direct record that invokes three prior results establishing zero cost at r=1, positive cost on any deviation, and strict inequality of costs.
Claim. The Nash equilibrium certificate is the structure whose fields assert that the recognition cost satisfies $J(1)=0$, that $J(r)>0$ for every $r>0$ with $r≠1$, and that $J(1)<J(r)$ for every $r>0$ with $r≠1$.
background
Recognition Science models agent decisions by minimization of the recognition cost function J, where the argument r is the ratio of an agent's action to the prevailing social norm. The module shows that Nash equilibrium in symmetric games coincides with the joint minimum of this cost, which occurs uniquely at r=1 for all agents. The structure NashEquilibriumCert packages the three properties required to certify this equilibrium: zero cost at the homeostatic point, positive cost for any unilateral deviation, and strict cost increase relative to the minimum. Upstream results supply the zero-cost identity Jcost 1 = 0, the positivity statement that Jcost r > 0 whenever r ≠ 1, and the stability comparison obtained by rewriting the zero-cost identity into the positivity statement.
proof idea
The definition is a direct record construction that populates the three fields of NashEquilibriumCert by assigning joint_homeostasis_zero_cost to the homeostasis_optimal field, deviation_increases_cost to the deviation_costly field, and nash_stability_at_homeostasis to the stability field.
why it matters
This declaration supplies the decision-theoretic foundation for the Nash equilibrium certificate used by the Economics module's type enumeration and by the master GameTheory certificate. It realizes the module's structural claim that Nash equilibrium equals the joint J-cost minimum at r=1, with any deviation strictly increasing cost. The result thereby links the upstream J-cost positivity and zero-at-unit theorems to game-theoretic stability in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.