Nondegenerate stock and bank holdings make a hedge unique

Proved

FinancialDerivatives.FD02.replicatingTrade_unique

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

arbitrageformal-verificationoption-pricing

If two stock-and-bank portfolios deliver the same terminal claim, their share holdings agree because the stock factors differ, and their cash holdings then agree because bank growth is positive.

A proof must use the exact published definitions and be accepted by the authoritative Prove2Me compiler.

Preamble

import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_Trade
import Definitions.Def_fd02_terminalPayoff
import Definitions.Def_fd02_Replicates

Formal statement

namespace FinancialDerivatives.FD02

/-- Nondegenerate stock and bank holdings make a hedge unique. -/
theorem replicatingTrade_unique (m : TwoStateMarket) (H : Bool → ℝ) (a b : Trade) (ha : Replicates m a H) (hb : Replicates m b H) :
  a = b := by sorry

end FinancialDerivatives.FD02

Source

Original derived theorem based on Wilmott, Howison and Dewynne (1995), §§2.4,3.2, pp. 30–34; 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$ , any real two-state claim $H$ with payoffs $H_+$ and $H_-$ , and any two signed trades $a=(x_a,c_a)$ and $b=(x_b,c_b)$ , if $x_aSU+c_aR=H_+$ , $x_aSD+c_aR=H_-$ , $x_bSU+c_bR=H_+$ , and $x_bSD+c_bR=H_-$ , then the trades are equal as records: $x_a=x_b$ and $c_a=c_b$ .

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