Henstock–Kurzweil Path Integral in Financial Mathematics: A Machine-Verified Pricing of European and Barrier Options

We apply the Gaussian-kernel Henstock–Kurzweil (HK) path-integral machinery developed in earlier parts of this programme to the first major application outside quantum mechanics: the Black–Scholes formula for European option pricing. Under the risk-neutral measure, the log-price x_t = log S_t is a Brownian motion with drift ν = r − σ²/2 and volatility σ > 0; its transition density is the Gaussian kernel with drift: G_t(x,y) = (2πσ²t)^(−1/2) exp(−(y − x − νt)²/(2σ²t)), t > 0. We give a complete, machine-checked Lean 4 / Mathlib formalization of the construction:- the Chapman–Kolmogorov (semigroup) law: ∫_ℝ G_s(x,z) G_t(z,y) dz = G_{s+t}(x,y);- the fact that G_t is a probability density;- the strong continuity of the evolution operator (P_t ψ)(x) = ∫_ℝ G_t(x,y) ψ(y) dy;- and the closed-form price of a European call obtained directly from the kernel: C = e^(−rT) ∫_ℝ max(e^y − K, 0) G_T(log S_0, y) dy = S_0 N(d₁) − K e^(−rT) N(d₂), with standard d₁, d₂ and N the standard normal CDF. We also show that the drift–diffusion Chernoff splitting is exact at every level, giving a rigorous path-integral derivation. All statements in the accompanying file HkBlackScholes.lean are sorry-free and depend only on the standard axioms propext, Classical.choice, Quot.sound.