Martingale calibration uniquely fixes the risk-neutral weight

Proved

FinancialDerivatives.FD02.riskNeutral_martingale_unique_bridge

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

arbitrageformal-verificationoption-pricing

Any real weight satisfying the one-step stock martingale equation equals (R-d)/(u-d), because the stock returns differ.

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_riskNeutralUp

Formal statement

namespace FinancialDerivatives.FD02

/-- Martingale calibration uniquely fixes the risk-neutral weight. -/
theorem riskNeutral_martingale_unique_bridge (m : TwoStateMarket) (w : ℝ) (h : w * m.up + (1 - w) * m.down = m.growth) :
  w = riskNeutralUp m := by sorry

end FinancialDerivatives.FD02

Source

Derived from Wilmott, Howison and Dewynne (1995), §10.2, equation (10.4), p. 183. 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 real number $w$ , if $wU+(1-w)D=R$ , then necessarily $w=(R-D)/(U-D)$ . There is no restriction on the sign or size of $w$ ; the denominator $U-D$ is nonzero by the market constraint.

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