One-period replication, unique quote and FD-01 risk-neutral pricing

Proved

FinancialDerivatives.FD02.unique_replication_noArbitrage_pricing

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

arbitrageformal-verificationoption-pricing

For an arbitrary signed terminal claim, prove a unique stock/cash replicator, a unique arbitrage-free derivative quote, and a constructed FD-01 state-price operator that agrees with discounted risk-neutral valuation and characterises all permitted quotes.

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
import Definitions.Def_fd02_Trade
import Definitions.Def_fd02_Replicates
import Definitions.Def_fd02_NoArbitrage
import Definitions.Def_fd02_ClaimNoArbitrage

Formal statement

namespace FinancialDerivatives.FD02

/-- One-period replication, unique quote and FD-01 risk-neutral pricing. -/
theorem unique_replication_noArbitrage_pricing (m : TwoStateMarket) (hNA : NoArbitrage m) (H : Bool → ℝ) :
  (∃! t : Trade, Replicates m t H) ∧ (∃! p : ℝ, ClaimNoArbitrage m H p) ∧ (∃ sys : FinancialDerivatives.FD01.FinitePriceSystem Bool, sys.statePrice true = riskNeutralUp m / m.growth ∧ sys.statePrice false = (1 - riskNeutralUp m) / m.growth ∧ sys.price H = riskNeutralValue m H ∧ (∀ p : ℝ, ClaimNoArbitrage m H p ↔ p = sys.price H)) := by sorry

end FinancialDerivatives.FD02

Source

Wilmott, Howison and Dewynne (1995), §§2.4,3.2,10.1–10.3, pp. 30–34 and 180–187; 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$ , assume the base-market no-arbitrage property that every signed real pair $(x,c)$ with $xS+c=0$ , $xSU+cR\ge0$ , and $xSD+cR\ge0$ has $xSU+cR=0$ and $xSD+cR=0$ , and let $H$ be any two-state real claim with payoffs $H_+,H_-$ and $q=(R-D)/(U-D)$ and $V=(qH_++(1-q)H_-)/R$ . All three assertions hold simultaneously: first, there is exactly one signed real pair $(x,c)$ whose terminal payoffs satisfy $xSU+cR=H_+$ and $xSD+cR=H_-$ ; second, there is exactly one real quote $p$ for which for every signed real stock holding $x$ , cash holding $c$ , and claim quantity $a$ , the conditions $xS+c+ap=0$ , $xSU+cR+aH_+\ge0$ , and $xSD+cR+aH_-\ge0$ imply $xSU+cR+aH_+=0$ and $xSD+cR+aH_-=0$ ; third, there exists a finite two-state price system with nonnegative state prices, strictly positive discount factor equal to their sum, true-state price $q/R$ , and false-state price $(1-q)/R$ (hence discount $1/R$ ), whose valuation $(q/R)H_++((1-q)/R)H_-$ equals $V$ and for which, for every real quote $p$ , the combined-market condition that for every signed real stock holding $x$ , cash holding $c$ , and claim quantity $a$ , the conditions $xS+c+ap=0$ , $xSU+cR+aH_+\ge0$ , and $xSD+cR+aH_-\ge0$ imply $xSU+cR+aH_+=0$ and $xSD+cR+aH_-=0$ holds exactly when $p$ equals that system's valuation of $H$ .

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