An attainable claim has exactly one arbitrage-free quoted price

Proved

FinancialDerivatives.FD02.claim_noArbitrage_iff_riskNeutralPrice

by WillR · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

arbitrageformal-verificationoption-pricing

In a strictly arbitrage-free complete two-state market, allowing trade in a claim preserves the no-arbitrage condition exactly at its replicating price, which equals discounted risk-neutral expectation.

A proof must use the exact published definitions and be accepted by the authoritative Prove2Me compiler.

Preamble

import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_Trade
import Definitions.Def_fd02_terminalPayoff
import Definitions.Def_fd02_Replicates
import Definitions.Def_fd02_replicatingTrade
import Definitions.Def_fd02_initialCost
import Definitions.Def_fd02_riskNeutralUp
import Definitions.Def_fd02_riskNeutralValue
import Definitions.Def_fd02_NoArbitrage
import Definitions.Def_fd02_ClaimNoArbitrage

Formal statement

namespace FinancialDerivatives.FD02

/-- An attainable claim has exactly one arbitrage-free quoted price. -/
theorem claim_noArbitrage_iff_riskNeutralPrice (m : TwoStateMarket) (hNA : NoArbitrage m) (H : Bool → ℝ) (p : ℝ) :
  ClaimNoArbitrage m H p ↔ p = riskNeutralValue m H := by sorry

end FinancialDerivatives.FD02

Source

Original derived theorem based on Wilmott, Howison and Dewynne (1995), §§3.2,10.1–10.3, pp. 33–34 and 180–187; https://doi.org/10.1017/CBO9780511812545.

Read-back

What the Lean code literally says, in plain math · GPT-6

For any market with real spot $S>0$ , bank growth $R>0$ , and stock factors $0\le D<U$ , if the base-market no-arbitrage property every signed real pair $(x,c)$ with $xS+c=0$ , $xSU+cR\ge0$ , and $xSD+cR\ge0$ has $xSU+cR=0$ and $xSD+cR=0$ holds, then for any real two-state claim $H$ with payoffs $H_+,H_-$ , $q=(R-D)/(U-D)$ and $V=(qH_++(1-q)H_-)/R$ , and any real quotation $p$ , the following are equivalent: (i) for every signed real stock holding $x$ , cash holding $c$ , and claim quantity $a$ , the conditions $xS+c+ap=0$ , $xSU+cR+aH_+\ge0$ , and $xSD+cR+aH_-\ge0$ imply $xSU+cR+aH_+=0$ and $xSD+cR+aH_-=0$ ; (ii) $p=V$ . Thus the equivalence concerns all real quotations and permits signed positions in both the stock and claim.

Human review

Endorsed by Shuze Chen · Oct 27, 2026
Confirmed by the moderator at approval.
Endorsed by WillR · Oct 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph