MarketEquilibrium
MarketEquilibrium defines the market equilibrium condition as the vanishing of J-cost at unit scale. Cross-domain researchers in Recognition Science cite it to equate market clearing with Nash and homeostasis equilibria under a single cost function. The definition is a direct abbreviation of the upstream Jcost_unit0 result.
claimMarket equilibrium holds precisely when the J-cost function satisfies $J(1) = 0$.
background
The CrossDomain.JEquilibriumUniversality module introduces three equilibrium propositions that all reduce to the same J-cost condition. Jcost is imported from IndisputableMonolith.Cost and satisfies Jcost_unit0, the lemma establishing that cost vanishes at scale factor 1. The module documentation states that Nash equilibrium, market equilibrium, and health equilibrium (homeostasis) are definitionally identical via this shared line.
proof idea
This is a definition that directly sets MarketEquilibrium to the proposition Jcost 1 = 0, serving as a one-line abbreviation.
why it matters in Recognition Science
The definition supplies the market instance of the J-equilibrium condition used in downstream results such as nash_eq_market, market_eq_health, and all_three_equal. It completes the C7 universality claim that the same Jcost 1 = 0 line governs game theory, efficient markets, and biological homeostasis. Within the Recognition framework it instantiates the shared sensitivity at equilibrium across domains, consistent with the Recognition Composition Law.
scope and limits
- Does not prove Jcost 1 = 0; that fact is supplied by the upstream Jcost_unit0 lemma.
- Does not compute the Hessian or perturbation multipliers; those appear only in the universality certificate.
- Does not extend the equivalence to domains outside the three listed in the module documentation.
formal statement (Lean)
33def MarketEquilibrium : Prop := Jcost 1 = 0