cert
plain-language theorem explainer
The declaration supplies a concrete certificate asserting that J-cost deviation vanishes exactly at price equilibrium, stays nonnegative off equilibrium, and that the significance threshold exceeds unity. Economists or Recognition Science researchers modeling arbitrage corrections would cite this when connecting the J-function to observed reversion scales. It assembles three prior theorems into the MarketEquilibriumCert structure with no extra steps.
Claim. Let deviation$(p,e)$ denote the J-cost of the price ratio $p/e$. The certificate asserts that deviation$(p,p)=0$ for all nonzero $p$, that deviation$(p,e)geq 0$ for all positive $p$ and $e$, and that the significance threshold exceeds 1.
background
The module treats market equilibrium as the state where price clears supply against demand. Departure from equilibrium incurs a J-cost: overshooting costs J$(p/p^)$ while undershooting costs the symmetric J$(p^/p)$. The deviation function is the J-cost of the ratio $p/e$, with J defined by the uniqueness property J$(x)=(x+x^{-1})/2-1$. The structure MarketEquilibriumCert packages three properties: exact vanishing at equilibrium, nonnegativity for positive arguments, and threshold strictly larger than one. Upstream theorems reduce the ratio to unity and invoke Jcost_unit0, apply Jcost_nonneg to the positive ratio, and reduce the threshold claim to one_lt_phi.
proof idea
The definition constructs an instance of MarketEquilibriumCert by directly assigning its three fields to the theorems priceDeviation_at_equilibrium, priceDeviation_nonneg, and priceSignificanceThreshold_gt_one.
why it matters
This definition realizes the structural theorem for market equilibrium derived from J-cost. It encodes the RS prediction that a price ratio of order phi marks the canonical significant departure, matching the phi-ladder at rung 1 and the eight-tick octave scaling. The module doc supplies the falsifier: any commodity study showing median reversion times outside the phi-ladder window at the 1-rung level. No downstream uses appear yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.