MarketEquilibriumCert
plain-language theorem explainer
MarketEquilibriumCert bundles three properties of the J-cost price deviation: it vanishes exactly when price equals equilibrium price, stays nonnegative for positive arguments, and the significance threshold exceeds one. Economists or econophysicists modeling arbitrage corrections would cite the structure when embedding Recognition Science cost functions into equilibrium models. The definition is a direct record that packages three upstream lemmas on priceDeviation and priceSignificanceThreshold with no additional steps.
Claim. A market equilibrium certificate under J-cost is a structure asserting: (i) the J-cost deviation on the price ratio vanishes when price equals equilibrium price, (ii) the deviation is nonnegative for all positive prices and equilibria, (iii) the significance threshold exceeds 1.
background
The module derives market equilibrium from the J-cost function. Price deviation is defined as the J-cost of the ratio of observed price to equilibrium price. The significance threshold is fixed at the golden ratio phi, corresponding to a roughly 62 percent departure that triggers noticeable arbitrage. Upstream results supply the concrete definitions: priceDeviation(p, e) equals Jcost(p/e) and priceSignificanceThreshold equals phi. The local setting predicts that departures larger than this threshold produce the minimum noticeable J-cost of J(phi) approximately 0.118, consistent with empirical reversion thresholds reported by Fama and Lo.
proof idea
The structure is defined by direct field assignment to the three lemmas priceDeviation_at_equilibrium, priceDeviation_nonneg, and priceSignificanceThreshold_gt_one.
why it matters
This certificate supplies the structural theorem for the market equilibrium model. It is instantiated by the cert definition and shown inhabited by cert_inhabited. The construction fills the zero-sorry structural slot in the Econ module, linking J-cost directly to observed commodity-market reversion thresholds at the phi-ladder level. It touches the module falsifier on median reversion times lying outside the one-rung phi prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.