Too-high bank growth gives an explicit arbitrage

Proved

FinancialDerivatives.FD02.arb_if_up_le_growth

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

arbitrageformal-verificationoption-pricing

If the up stock factor does not exceed bank growth, shorting shares and depositing the proceeds gives a zero-cost nonnegative terminal payoff, strictly positive in the down state.

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

Formal statement

namespace FinancialDerivatives.FD02

/-- Too-high bank growth gives an explicit arbitrage. -/
theorem arb_if_up_le_growth (m : TwoStateMarket) (h : m.up ≤ m.growth) :
  ¬ NoArbitrage m := 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$ with the additional hypothesis $U\le R$ , the market fails the following zero-cost no-arbitrage property: every signed real pair $(x,c)$ with $xS+c=0$ , $xSU+cR\ge0$ , and $xSD+cR\ge0$ has $xSU+cR=0$ and $xSD+cR=0$ . Equivalently, some signed real holdings $(x,c)$ have zero cost, nonnegative payoff in both Boolean states, and strictly positive payoff in at least one; equality $U=R$ is included.

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