Put–call parity, forward form: $C - P = D(F - K)$

Proved

BlackScholesModel.put_call_parity_fwd

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

black-scholesmathematical-financeoption-pricing

For all real $D,F,K,\sigma,\tau$ , the forward-form (Black '76) call and put values $C(F,\tau)=D[N(d_+)F-N(d_-)K]$ and $P(F,\tau)=D[N(-d_-)K-N(-d_+)F]$ , with $d_\pm=\frac{1}{\sigma\sqrt\tau}\big[\ln\frac FK\pm\frac12\sigma^2\tau\big]$ , satisfy

C-P=D(F-K).

With $D=e^{-r\tau}$ and $F=S/D$ this reads $C-P=S-DK$ .

Formalization Note The identity holds for all real inputs, so no positivity hypotheses are imposed.

Preamble

import Mathlib
import Definitions.Def_BlackScholesModel_Core

open Real MeasureTheory ProbabilityTheory Filter Topology
open scoped ContDiff

Formal statement

namespace BlackScholesModel

theorem put_call_parity_fwd (D F K σ τ : ℝ) :
    callPriceFwd D F K σ τ - putPriceFwd D F K σ τ = D * (F - K) := by sorry

end BlackScholesModel

Source

Wikipedia, "Black–Scholes model" (snapshot supplied as Black–Scholes_model.pdf, 22 pp.), https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model; p. 4 (Alternative formulation: put–call parity C − P = D(F − K) = S − DK)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (at the explicit instruction of the proposal owner), not by an independent blind auditor. It is not independent testimony; reviewers should compare it against the Lean code themselves.

For all real numbers $D,F,K,\sigma,\tau$ , with no hypotheses,

\tilde C(D,F,K,\sigma,\tau)-\tilde P(D,F,K,\sigma,\tau)=D\,(F-K),

where $\tilde C=D\big(N(\tilde d_+)F-N(\tilde d_-)K\big)$ , $\tilde P=D\big(N(-\tilde d_-)K-N(-\tilde d_+)F\big)$ , $\tilde d_+=\frac{\ln(F/K)+\sigma^2\tau/2}{\sigma\sqrt\tau}$ and $\tilde d_-=\tilde d_+-\sigma\sqrt\tau$ (definition file, with the formal system's conventions for division by zero, square roots of negatives and logarithms of non-positive numbers), and $N$ is the normal distribution function.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by WillR · Oct 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Put–call parity, forward form: C−P=D(F−K)C - P = D(F - K)C−P=D(F−K)

Put–call parity, forward form: $C - P = D(F - K)$