Prove2Me

Every exact hedge has one common no-arbitrage cost

Proved
FinancialDerivatives.FD02.replicationCost_unique

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

arbitrageformal-verificationoption-pricing

If any trade reproduces the claim, its date-zero cost equals the discounted expectation computed from the unique risk-neutral stock weight.

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
Formal statement
namespace FinancialDerivatives.FD02

/-- Every exact hedge has one common no-arbitrage cost. -/
theorem replicationCost_unique (m : TwoStateMarket) (H : Bool → ℝ) (t : Trade) (ht : Replicates m t H) :
  initialCost m t = riskNeutralValue m H := by sorry

end FinancialDerivatives.FD02
Source
Original derived theorem based on Wilmott, Howison and Dewynne (1995), §§3.2,10.3, pp. 33–34 and 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>0S>0, bank growth R>0R>0, and stock factors 0≤D<U0\le D<U, any real two-state claim HH with payoffs H+H_+ and H−H_- and q=(R−D)/(U−D)q=(R-D)/(U-D) and V=(qH++(1−q)H−)/RV=(qH_++(1-q)H_-)/R, every signed trade (x,c)(x,c) satisfying both xSU+cR=H+xSU+cR=H_+ and xSD+cR=H−xSD+cR=H_- has initial cost xS+c=VxS+c=V. The statement imposes neither no-arbitrage nor positivity of claim payoffs or the weight qq.

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