nash_eq_market
plain-language theorem explainer
The declaration equates the Nash equilibrium proposition with the market equilibrium proposition in the J-cost framework. A researcher transferring results between game theory and efficient-market models would cite it to justify shared perturbation analysis. The proof is a one-line reflexivity that follows because both propositions are defined identically as Jcost 1 = 0.
Claim. The Nash equilibrium proposition equals the market equilibrium proposition, where each is the assertion that the unit J-cost vanishes: $Jcost(1) = 0$.
background
The J-Equilibrium Universality module shows that equilibrium conditions drawn from game theory, economics, and biology all reduce to one core statement. NashEquilibrium is defined as the proposition Jcost 1 = 0; MarketEquilibrium carries the identical definition. The module doc states that each is a specialisation of Jcost 1 = 0 to a domain label and that Lean sees them as literally the same theorem.
proof idea
The proof is a one-line wrapper that applies reflexivity to the shared definition Jcost 1 = 0.
why it matters
This theorem supplies one link in the C7 universality witness that the same Jcost 1 = 0 condition serves as equilibrium across three fields. It thereby supports the module consequence that the Hessian of J at unit scale yields the same multiplier in each domain. The declaration closes part of the structural claim that all three propositions are definitionally identical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.