MarketEquilibrium
plain-language theorem explainer
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.
Claim. Market 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.