market_equilibrium
plain-language theorem explainer
The declaration asserts that the J-cost function evaluates to zero at argument one, encoding market equilibrium in the Recognition Science model of financial markets. Economists applying RS to asset pricing would cite this as the base case for the efficient-market condition where deviations close toward zero. The proof is a direct one-line application of the unit lemma for Jcost via simplification.
Claim. $J(1) = 0$ where $J(x) = (x-1)^2 / (2x)$.
background
In Recognition Science the J-cost function quantifies deviation from equilibrium and is given by the squared-ratio form $J(x) = (x-1)^2 / (2x)$. The module FinancialMarketsFromRS maps this cost to economics by equating five canonical asset classes to configuration dimension D = 5 and defining financial equilibrium precisely as the vanishing of J. The upstream lemma Jcost_unit0 supplies the identity by direct simplification of the Jcost definition.
proof idea
This is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
The result is referenced inside the FinancialMarketsCert definition to certify the five asset classes, five risks, and equilibrium condition. It supplies the equilibrium step that links the RS cost model to the efficient-market hypothesis in which J > 0 gaps close toward zero. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.