nash_eq
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.