Henstock–Kurzweil Path Integral in Financial Mathematics: A Machine-Verified Pricing of European and Barrier Options
Alexander S. Ushakov, Yury N. Berdinsky
q-fin.PR
Jul 26, 2026 · v1
TL;DR
Formalizes the Gaussian transition kernel, Chapman–Kolmogorov semigroup law, strong continuity, the Black–Scholes call formula and an exact Chernoff product in Lean 4/Mathlib, sorry-free.
Abstract
We apply the Henstock–Kurzweil (HK) gauge integral to the Black–Scholes model of option pricing and obtain the European call price directly from a Gaussian cylindrical kernel, without stochastic calculus. Under the risk- neutral measure, the log-price is a Brownian motion with drift nu = r - sigma^2/2. Its transition density is the Gaussian kernel G_t(x,y) = (2 pi sigma^2 t)^{-1/2} exp( - (y - x - nu t)^2 / (2 sigma^2 t) ). We give a machine-checked formalization in Lean 4 / Mathlib of the following: the Chapman–Kolmogorov (semigroup) property, the fact that G_t is a probability density, strong continuity of the pricing operator, the closed-form price C = S_0 N(d_1) - K e^{-rT} N(d_2) with the standard normal CDF N, and the exactness of the drift–diffusion Chernoff splitting at every level. The entire proof is "sorry"-free and depends only on propext, Classical.choice, and Quot.sound. Digital and barrier options are treated as further examples, illustrating the universality of the method, and we show that the construction is compatible with the classical Ito calculus in the continuum limit.
Problem
Option pricing in the Black–Scholes model is usually derived with stochastic calculus. The authors seek a derivation of the European call price directly from a Gaussian cylindrical kernel within a Henstock–Kurzweil gauge-integral framework, with every step machine-verified.
Approach
The log-price is modelled as a Brownian motion with drift, whose transition density is a Gaussian kernel. Its total mass, the Chapman–Kolmogorov semigroup property, a Girsanov-type drift-shift invariance and strong continuity of the pricing operator are proved, followed by the closed-form call price from two Gaussian tail integrals. Exactness of the drift–diffusion Chernoff splitting is proved by induction from the semigroup law. All of these are formalized in a Lean 4/Mathlib file, HkBlackScholes.lean.
Results
The formalization is sorry-free, and each headline theorem depends only on propext, Classical.choice and Quot.sound. Digital call and barrier options are worked out as further examples, and the construction is argued to agree with Itô calculus in the continuum limit.
