Prove2Me

Exact payoff replication in both states

Definition
fd02_Replicates

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

arbitrageformal-verificationoption-pricing

Exact replication requires equality of the portfolio and contingent-claim payoffs in both terminal states.

Definition code
import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_Trade
import Definitions.Def_fd02_terminalPayoff

namespace FinancialDerivatives.FD02

/-- A trade replicates a claim if its payoff matches in each state. -/
def Replicates (m : TwoStateMarket) (t : Trade) (H : Bool → ℝ) : Prop :=
  ∀ ω : Bool, terminalPayoff m t ω = H ω

end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §2.4 and §10.3, printed pp. 30–31 and 187; https://doi.org/10.1017/CBO9780511812545. The same object is fixed for all FD-02 theorem statements.
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, a signed trade (x,c)(x,c), and any claim H:{false,true}→RH:\{\mathrm{false},\mathrm{true}\}\to\mathbb R, the predicate “replicates HH” holds exactly when both xSU+cR=H(true)xSU+cR=H(\mathrm{true}) and xSD+cR=H(false)xSD+cR=H(\mathrm{false}). Every Boolean state must match; either claim payoff may have any real sign.

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