priceDeviation
plain-language theorem explainer
priceDeviation computes the recognition cost of a price ratio as the measure of departure from market equilibrium. Market modelers and arbitrage theorists cite it when quantifying how far an observed price strays from clearing value. The definition is a direct one-line application of the Jcost function to the normalized ratio.
Claim. For observed price $p$ and equilibrium price $p^*$, the deviation cost is $J(p/p^*)$, where $J$ is the recognition cost function.
background
The module develops market equilibrium from the J-cost framework. Market equilibrium occurs when price clears supply equal to demand. Any departure incurs a J-cost: overshooting costs $J(p/p^)$ while undershooting costs the symmetric value $J(p^/p) = J(p/p^*)$ by the properties of $J$. The module states that the minimum noticeable deviation corresponds to $J(φ) ≈ 0.118$, or roughly a 62% shift from equilibrium, aligning with empirical reversion thresholds reported by Fama and Lo.
proof idea
This is a direct definition that applies the Jcost function to the ratio price / equilibrium_price. No lemmas or tactics are required beyond the unfolding of the abbreviation.
why it matters
The definition supplies the deviation measure used inside MarketEquilibriumCert, which records that the cost vanishes at equilibrium and remains nonnegative otherwise. It also supports the explicit threshold theorem priceSignificanceThreshold_gt_one. The construction realizes the Recognition Science prediction that significant departures begin at the φ rung of the cost ladder, furnishing the econ-side counterpart to the J-uniqueness and phi-fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.