MarketArbitrageGap
plain-language theorem explainer
MarketArbitrageGap defines the proposition that J-cost is strictly positive for every positive real r not equal to one. Market theorists cite it as the recognition-science expression of arbitrage opportunity arising from price or return deviations. The definition is a direct domain specialisation of the universal Jcost positivity statement, identical in form to the six other cross-domain costs.
Claim. Market arbitrage gap is the statement that for every positive real number $r$ with $r ≠ 1$, the J-cost satisfies $J(r) > 0$, where $J(r) = (r + r^{-1})/2 - 1$.
background
In Recognition Science the J-cost function quantifies deviation from equilibrium through the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Module C16 establishes that this cost is positive for any r in (0, ∞) with r ≠ 1, supplying a uniform source of non-equilibrium cost across domains. MarketArbitrageGap is the financial-market specialisation of the same universal positivity proposition that also appears as TurbulentCost, DiseaseCost and the other five labels.
proof idea
This is a definition that directly instantiates the universal positivity statement for the market domain. It is applied verbatim by the one-line wrapper theorem market_arbitrage_gap, which invokes Jcost_pos_of_ne_one.
why it matters
The definition supplies the market-specific label for the universal non-equilibrium cost claim. It is collected inside JPositivityUniversalityCert and shown definitionally equal to the other six costs by all_seven_are_one. Within the framework it realises the off-equilibrium analogue of C7, extending J-uniqueness (T5) to cross-domain applications that include arbitrage gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.