Too-low bank growth gives an explicit arbitrage

Proved

FinancialDerivatives.FD02.arb_if_growth_le_down

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

arbitrageformal-verificationoption-pricing

If bank growth is no greater than the down stock factor, buying shares with borrowed cash costs zero and pays nonnegatively in both states and strictly positively in the up 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-low bank growth gives an explicit arbitrage. -/
theorem arb_if_growth_le_down (m : TwoStateMarket) (h : m.growth ≤ m.down) :
  ¬ 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 $R\le D$ , 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 terminal payoff in both Boolean states, and a strictly positive payoff in at least one state; equality $R=D$ 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