priceDeviation_nonneg
plain-language theorem explainer
The theorem shows that the J-cost on any positive price ratio is nonnegative. Modelers of market arbitrage and equilibrium would cite it when bounding deviation penalties in RS-based pricing. The proof is a direct one-line wrapper that unfolds the price ratio definition and invokes Jcost nonnegativity on the positive quotient p/e.
Claim. Let $p > 0$ and $e > 0$ be real numbers. Then $0 ≤ J(p/e)$, where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function.
background
The module MarketEquilibriumFromJCost treats market clearing as the point where price deviation carries a J-cost. priceDeviation is defined as Jcost(p/e), so overshooting or undershooting the equilibrium price e incurs the same nonnegative penalty by symmetry of J. The J-cost satisfies J(x) ≥ 0 for x > 0 by the AM-GM inequality x + 1/x ≥ 2, which is the content of the upstream Jcost_nonneg lemmas.
proof idea
The proof unfolds priceDeviation to expose Jcost(p/e) and applies the lemma Jcost_nonneg to the ratio p/e, which is positive by div_pos hp he.
why it matters
It supplies the nonnegativity axiom for MarketEquilibriumCert, the top-level certification object that also collects deviation_at_equilibrium and threshold_gt_one. This completes the structural theorem for RS market equilibrium, linking directly to J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain. The result underpins the prediction that noticeable departures begin at J(φ) ≈ 0.118, matching the 50-60% empirical arbitrage threshold cited in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.