Prove2Me

Two state prices add to the unit cash discount factor

Proved
FinancialDerivatives.FD02.statePrices_sum_discount

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

arbitrageformal-verificationoption-pricing

The total Arrow–Debreu price of the constant one-unit terminal payoff is the bank discount factor 1/R.

This is an original derived theorem target; a remote compiler must validate its declaration and proof.

Preamble
import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_riskNeutralUp
Formal statement
namespace FinancialDerivatives.FD02

/-- Two state prices add to the unit cash discount factor. -/
theorem statePrices_sum_discount (m : TwoStateMarket) :
  riskNeutralUp m / m.growth + (1 - riskNeutralUp m) / m.growth = 1 / m.growth := by sorry

end FinancialDerivatives.FD02
Source
Derived from Wilmott, Howison and Dewynne (1995), §10.1, equation (10.2), p. 182. 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 and q=(R−D)/(U−D)q=(R-D)/(U-D), the two real expressions q/Rq/R and (1−q)/R(1-q)/R sum to exactly 1/R1/R: q/R+(1−q)/R=1/Rq/R+(1-q)/R=1/R. No no-arbitrage or positivity assumption on qq is required.

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