Prove2Me

Constructed FD-01 valuation agrees with the two-state expectation

Proved
FinancialDerivatives.FD02.FD01_price_eq_riskNeutralValue

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

arbitrageformal-verificationoption-pricing

The actual FD-01 finite-price system built from positive two-state weights values every signed payoff at its one-period discounted risk-neutral expectation.

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 FD-01 valuation agrees with the two-state expectation. -/
theorem FD01_price_eq_riskNeutralValue (m : TwoStateMarket) (hq0 : 0 < riskNeutralUp m) (hq1 : riskNeutralUp m < 1) (H : Bool → ℝ) :
  (toFD01PriceSystem m hq0 hq1).price H = riskNeutralValue m H := by sorry

end FinancialDerivatives.FD02
Source
Wilmott, Howison and Dewynne (1995), §10.1, equation (10.2), p. 182; 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>0S>0, bank growth R>0R>0, and stock factors 0≤D<U0\le D<U, q=(R−D)/(U−D)q=(R-D)/(U-D) with additional hypotheses 0<q<10<q<1, and any real-valued claim HH with true and false payoffs H+H_+ and H−H_-, let the constructed finite price system have true-state price q/Rq/R, false-state price (1−q)/R(1-q)/R, and discount 1/R1/R. Then its price of HH, the sum (q/R)H++((1−q)/R)H−(q/R)H_++((1-q)/R)H_-, equals the defined discounted expression (qH++(1−q)H−)/R\big(qH_++(1-q)H_-\big)/R.

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