Constructed state prices correctly value one bank deposit

Proved

FinancialDerivatives.FD02.statePrices_bank_calibration

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

arbitrageformal-verificationoption-pricing

The positive Arrow–Debreu prices value the bank-account claim paying R in either state at exactly its initial unit cost.

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 one bank deposit. -/
theorem statePrices_bank_calibration (m : TwoStateMarket) (hq0 : 0 < riskNeutralUp m) (hq1 : riskNeutralUp m < 1) :
  (toFD01PriceSystem m hq0 hq1).price (fun _ : Bool => m.growth) = 1 := by sorry

end FinancialDerivatives.FD02

Source

Wilmott, Howison and Dewynne (1995), §§3.2,10.1, pp. 33–34 and 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>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 state prices $q/R$ to true and $(1-q)/R$ to false, with positive discount factor $1/R$ and state-price sum $1/R$ . Valuing a claim by the sum of each state price times its state payoff, this system assigns value one to the constant payoff $R$ in each state: $(q/R)R+((1-q)/R)R=1$ .

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