Constructed state prices correctly value the share

Proved

FinancialDerivatives.FD02.statePrices_stock_calibration

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

arbitrageformal-verificationoption-pricing

Under the unique martingale weights, the FD-01 price of the stock's up/down terminal payoffs equals its initial share price S0.

This is an original derived proof obligation in the private FD-02 authoring graph.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Definitions.Def_fd01_FinitePriceSystem
import Definitions.Def_fd01_price
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_riskNeutralUp
import Definitions.Def_fd02_riskNeutralValue
import Definitions.Def_fd02_toFD01PriceSystem

Formal statement

namespace FinancialDerivatives.FD02

/-- Constructed state prices correctly value the share. -/
theorem statePrices_stock_calibration (m : TwoStateMarket) (hq0 : 0 < riskNeutralUp m) (hq1 : riskNeutralUp m < 1) :
  (toFD01PriceSystem m hq0 hq1).price (fun ω : Bool => if ω then m.spot * m.up else m.spot * m.down) = m.spot := by sorry

end FinancialDerivatives.FD02

Source

Wilmott, Howison and Dewynne (1995), §10.2, equation (10.4), pp. 183–184; original finite-market formalisation. 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$ and $q=(R-D)/(U-D)$ under the two additional hypotheses $0<q<1$ , construct the two-state price system assigning prices $q/R$ to true and $(1-q)/R$ to false, with positive discount $1/R$ and total state price $1/R$ . Its state-price valuation of the two-state payoff $SU$ in the true state and $SD$ in the false state equals the initial spot price: $(q/R)SU+((1-q)/R)SD=S$ .

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