NashEquilibrium
plain-language theorem explainer
NashEquilibrium is defined as the proposition that Jcost at 1 equals zero. Game theorists and cross-domain modelers cite it to treat Nash equilibrium as identical to market and health equilibria under one cost function. The definition is a direct abbreviation with no proof body, enabling reflexivity to equate the three domains in Lean.
Claim. The Nash equilibrium condition is the proposition $J(1)=0$, where $J$ denotes the J-cost function.
background
The module constructs J-Equilibrium Universality for Wave 62 Cross-Domain. It shows that the equilibrium condition in Nash games, efficient markets, and biological homeostasis all reduce to the same proposition. The module doc states: 'the same Lean theorem (Jcost 1 = 0) is the equilibrium condition in three a priori distinct fields' and notes that perturbations of J produce the same multiplier across domains. The J-cost function is imported from the Cost module and satisfies the unit-scale lemma Jcost_unit0.
proof idea
The declaration is a definition that directly sets NashEquilibrium to the proposition Jcost 1 = 0. No lemmas or tactics are invoked; it functions as an abbreviation that lets downstream reflexivity proofs treat the three equilibria as identical.
why it matters
This definition anchors the JEquilibriumUniversalityCert structure and the theorem all_three_equal, which bundles the three equilibria and proves they coincide by reflexivity. It realizes the C7 structural claim that Nash, market, and health equilibria share the J-cost zero condition. The result connects to the Recognition framework by making the equilibrium at the self-similar fixed point universal, with shared sensitivity across domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.