priceDeviation_at_equilibrium
plain-language theorem explainer
The J-cost of price deviation vanishes exactly when observed price equals equilibrium price, for any nonzero real price level. Economists modeling arbitrage and market clearing would cite this to fix the zero baseline of the deviation measure. The proof is a one-line wrapper that unfolds the definition and reduces via the unit property of Jcost.
Claim. For any nonzero real number $p$, the J-cost of the price ratio equals zero: $Jcost(p/p)=0$, where $Jcost(x)=(x-1)^2/(2x)$.
background
The module derives market equilibrium from the J-cost on price ratios. priceDeviation is defined as Jcost(price / equilibrium_price). Upstream Jcost_unit0 asserts Jcost(1)=0, which follows immediately from the squared-ratio expression of J. The module setting treats equilibrium as the point where supply equals demand and any departure incurs a symmetric J-cost penalty on the ratio or its reciprocal.
proof idea
One-line wrapper that unfolds priceDeviation, rewrites the self-division by the nonzero hypothesis, and applies the Jcost_unit0 lemma.
why it matters
This supplies the deviation_at_eq field of MarketEquilibriumCert, anchoring the zero point of the econ application. It supports the structural claim that the minimum noticeable departure corresponds to J(φ) on the price ratio. The result closes the baseline in the Recognition framework's use of J-cost for market models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.