Terminal stock-and-cash payoffs are additive

Proved

FinancialDerivatives.FD02.terminalPayoff_add

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

arbitrageformal-verificationoption-pricing

For either terminal state, combining two trades adds their terminal cash payments.

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_Trade
import Definitions.Def_fd02_terminalPayoff

Formal statement

namespace FinancialDerivatives.FD02

/-- Terminal stock-and-cash payoffs are additive. -/
theorem terminalPayoff_add (m : TwoStateMarket) (a b : Trade) (ω : Bool) :
  terminalPayoff m ({ shares := a.shares + b.shares, cash := a.cash + b.cash } : Trade) ω = terminalPayoff m a ω + terminalPayoff m b ω := by sorry

end FinancialDerivatives.FD02

Source

Derived from Wilmott, Howison and Dewynne (1995), §2.4, pp. 30–31. 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 signed trades $a=(x_1,c_1)$ and $b=(x_2,c_2)$ , and either Boolean state, the componentwise-sum trade has payoff equal to the sum of their payoffs. Explicitly, $(x_1+x_2)SF+(c_1+c_2)R=(x_1SF+c_1R)+(x_2SF+c_2R)$ , where $F=U$ in the true state and $F=D$ in the false state.

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