market_eq
plain-language theorem explainer
Market equilibrium holds exactly when the J-cost vanishes at unit scale. Economists modeling efficient markets would cite this to equate price clearing with the recognition cost zero. The proof is a direct one-line assignment of the core lemma that simplifies Jcost at argument one.
Claim. Market equilibrium holds when $J(1)=0$, where $J(x)=((x-1)^2)/(2x)$.
background
The J-cost is defined as $J(x)=((x-1)^2)/(2x)$, which measures deviation from the fixed point at unity and vanishes there. The module states that this same zero condition supplies the equilibrium notion in Nash games, markets, and homeostasis. The upstream lemma Jcost_unit0 proves the evaluation at one by direct simplification of the squared-ratio form.
proof idea
One-line wrapper that applies the lemma Jcost_unit0, which reduces Jcost 1 to zero via simp on the squared-ratio definition.
why it matters
This theorem supplies the market component inside jEquilibriumUniversalityCert, the structure that bundles the three equilibria and their shared sensitivity. It realizes the C7 claim that the identical J-cost zero governs Nash, market, and health equilibria, with identical perturbation multipliers across domains. The result aligns with the Recognition Composition Law and the J-uniqueness fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.