Prove2Me

The hedge cost equals the discounted risk-neutral expectation

Proved
FinancialDerivatives.FD02.hedgeCost_eq_riskNeutralValue

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

arbitrageformal-verificationoption-pricing

The uniquely constructed stock-and-cash hedge costs (q H_up + (1-q) H_down)/R; this is an algebraic identity valid under the market nondegeneracy conditions.

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

/-- The hedge cost equals the discounted risk-neutral expectation. -/
theorem hedgeCost_eq_riskNeutralValue (m : TwoStateMarket) (H : Bool → ℝ) :
  initialCost m (replicatingTrade m H) = riskNeutralValue m H := by sorry

end FinancialDerivatives.FD02
Source
Original derived theorem based on Wilmott, Howison and Dewynne (1995), §10.1, equation (10.2), p. 182; §10.3, p. 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, let x=(H+−H−)/(S(U−D))x=(H_+-H_-)/(S(U-D)) and c=(UH−−DH+)/(R(U−D))c=(UH_--DH_+)/(R(U-D)) be the constructed signed trade. Its initial cost is the discounted weighted value: xS+c=VxS+c=V. This identity holds without a no-arbitrage hypothesis and without assuming qq lies between zero and one.

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