NashEquilibrium
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit form of the J-cost function.
- Does not prove Jcost 1 = 0; that is supplied by Jcost_unit0.
- Does not compute the Hessian or perturbation multipliers at equilibrium.
- Does not address scales other than unit or higher rungs on the phi-ladder.
Lean usage
theorem nash_eq : NashEquilibrium := Jcost_unit0formal statement (Lean)
32def NashEquilibrium : Prop := Jcost 1 = 0