nash_equilibrium
plain-language theorem explainer
The theorem states that the recognition cost J vanishes at scale 1, which the RS framework equates with Nash equilibrium. Game theorists or economists working inside the Recognition Science derivation would cite it as the cost-minimum fixed point linking classical equilibrium to J-cost. The proof is a direct term application of the unit lemma Jcost_unit0.
Claim. The recognition cost satisfies $J(1)=0$, where $J(x)=((x-1)^2)/(2x)$.
background
The module derives game theory from Recognition Science by identifying Nash equilibrium with the state of zero recognition cost, where no unilateral deviation improves payoff. J-cost is defined in the Cost module as the squared relative deviation $J(x)=((x-1)^2)/(2x)$, which is equivalent to the hyperbolic form from T5. The local setting treats five canonical game types as dimension-5 configurations and marks off-equilibrium states by J>0.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module (and its duplicate in JcostCore).
why it matters
This supplies the nash_eq field to the downstream gameTheoryCert definition, which packages the five game types together with the equilibrium and off-equilibrium markers. It realizes the module's claim that Nash equilibrium equals J=0 and thereby supplies the RS derivation of Nash's theorem. The result bridges the equilibrium theorem from NonlinearDynamicsFromRS to economic applications, closing the link from the J-uniqueness property to social-science fixed points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.