nash_eq
The nash_eq theorem asserts that the Nash equilibrium proposition holds by direct reduction to the vanishing of the J-cost at scale one. Researchers in game theory or cross-domain equilibrium analysis within Recognition Science would reference it to unify Nash, market, and health equilibria under a single cost function. The proof consists of a one-line assignment from the Jcost_unit0 lemma.
claimThe Nash equilibrium condition holds because $J(1)=0$, where $J(x)=((x-1)^2)/(2x)$.
background
In the CrossDomain.JEquilibriumUniversality module the framework posits that a single condition Jcost 1 = 0 serves as the equilibrium criterion across game theory (Nash), economics (market), and biology (health). The J-cost function is defined as J(x) = (x-1)^2 / (2x), which vanishes at x=1. This builds on the upstream Jcost_unit0 lemma, which establishes Jcost 1 = 0 by simplification. The module constructs a universality witness structure containing three propositions proved by the same core lemma.
proof idea
The proof is a one-line wrapper that directly invokes the Jcost_unit0 lemma from the Cost module, which itself simplifies the definition of Jcost to show it equals zero at argument one.
why it matters in Recognition Science
This theorem supplies the Nash component for the JEquilibriumUniversalityCert structure, which bundles the three equilibria and their shared sensitivity. It supports the GameTheoryCert in the Economics.GameTheoryFromRS module by providing the nash_eq field. Within the Recognition Science framework, it realizes the J-Equilibrium Universality claim (C7), showing that the same J-cost zero condition unifies equilibria across domains.
scope and limits
- Does not establish the existence of Nash equilibria for arbitrary payoff matrices.
- Does not compute the Hessian or perturbation multipliers explicitly.
- Does not derive the J-cost expression from the Recognition Composition Law.
- Does not address non-unit scales or off-equilibrium behavior.
Lean usage
theorem example : NashEquilibrium := nash_eqformal statement (Lean)
36theorem nash_eq : NashEquilibrium := Jcost_unit0