Every signed two-state claim has an exact hedge

Proved

FinancialDerivatives.FD02.replicatingTrade_exists

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

arbitrageformal-verificationoption-pricing

The explicit stock-and-bank portfolio replicates the entire payoff function on both Boolean terminal states.

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
import Definitions.Def_fd02_replicatingTrade

Formal statement

namespace FinancialDerivatives.FD02

/-- Every signed two-state claim has an exact hedge. -/
theorem replicatingTrade_exists (m : TwoStateMarket) (H : Bool → ℝ) :
  Replicates m (replicatingTrade m H) H := by sorry

end FinancialDerivatives.FD02

Source

Original derived theorem based on Wilmott, Howison and Dewynne (1995), §2.4, pp. 30–31 and §10.3, p. 187; 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 any two-state real claim $H$ with $H_+=H(\mathrm{true})$ and $H_-=H(\mathrm{false})$ , the specifically constructed trade $x=(H_+-H_-)/(S(U-D))$ shares and $c=(UH_--DH_+)/(R(U-D))$ cash replicates the claim in both Boolean states: $xSU+cR=H_+$ and $xSD+cR=H_-$ . The claim and the two holdings may be signed.

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