NashEquilibriumCert
plain-language theorem explainer
The NashEquilibriumCert structure packages three predicates on the J-cost function to certify that ratio one is the unique global minimum with value zero and that every other positive ratio yields strictly higher cost. Game theorists and decision theorists working inside the recognition science program cite this certificate to equate symmetric Nash equilibria with zero-cost recognition states. The structure is introduced directly by asserting the three fields on Jcost with no internal proof steps.
Claim. A certificate that the recognition cost function $J$ satisfies $J(1)=0$, that $J(r)>0$ for every $r>0$ with $r≠1$, and that $J(1)<J(r)$ whenever $r>0$ and $r≠1$.
background
The Decision module imports Jcost from the Cost module, where it measures the recognition cost of an agent's action ratio relative to the prevailing social norm. The module's local setting treats Nash equilibrium as the joint minimum of this cost across agents, which occurs precisely when every agent adopts ratio one. This follows the Tier F development in which equilibria are derived from the functional properties of J rather than from payoff matrices.
proof idea
The declaration is a structure definition that directly asserts the three fields on Jcost. No lemmas are invoked and no tactics are used; the fields themselves constitute the certificate.
why it matters
This certificate supplies the decision-theoretic instance of the Nash equilibrium from J-cost minimisation and is instantiated by the sibling definition nashEquilibriumCert. It realises the module claim that the unique zero-cost joint state is the equilibrium. In the framework it supports the derivation of recognitively stable equilibria from the J functional, consistent with the forcing chain that isolates the zero-cost fixed point at ratio one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.