Opposite trades have opposite costs

Proved

FinancialDerivatives.FD02.initialCost_neg

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

arbitrageformal-verificationoption-pricing

Shorting an existing stock-and-cash trade reverses its initial cost.

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

Formal statement

namespace FinancialDerivatives.FD02

/-- Opposite trades have opposite costs. -/
theorem initialCost_neg (m : TwoStateMarket) (t : Trade) :
  initialCost m ({ shares := -t.shares, cash := -t.cash } : Trade) = -initialCost m t := by sorry

end FinancialDerivatives.FD02

Source

Derived from Wilmott, Howison and Dewynne (1995), §3.2, pp. 33–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)$ , negating both holdings negates its initial cost: $(-x)S+(-c)=-(xS+c)$ . This applies without a nonnegativity condition on either holding or cost.

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