Zero-cost portfolios expose the stock excess returns

Proved

FinancialDerivatives.FD02.zeroCost_terminal_spread

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

arbitrageformal-verificationoption-pricing

If initial cost is zero, cash holdings offset the shares at today's price. Both terminal payments are then shares times the stock excess growth over the bank return.

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

Formal statement

namespace FinancialDerivatives.FD02

/-- Zero-cost portfolios expose the stock excess returns. -/
theorem zeroCost_terminal_spread (m : TwoStateMarket) (t : Trade) (h : initialCost m t = 0) :
  t.cash = -t.shares * m.spot ∧ terminalPayoff m t true = t.shares * m.spot * (m.up - m.growth) ∧ terminalPayoff m t false = t.shares * m.spot * (m.down - m.growth) := by sorry

end FinancialDerivatives.FD02

Source

Derived from 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$ and any signed trade $(x,c)$ whose initial cost vanishes, $xS+c=0$ , all three assertions hold together: $c=-xS$ , the true-state payoff $xSU+cR$ equals $xS(U-R)$ , and the false-state payoff $xSD+cR$ equals $xS(D-R)$ . No signs are assumed for these terminal payoffs.

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