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

Battle Count: 73

The paper is primarily a mathematical/proof-theoretic contribution to financial mathematics rather than a practical trading tool. It provides a rigorous, machine-verified derivation of the Black-Scholes formula, which is foundational for options pricing used in quantitative trading. However, it does not propose new trading strategies, empirical models, or computational tools for live trading. Its relevance is indirect: it strengthens the mathematical foundations upon which quantitative pricing models rest, and the formal verification aspect could increase confidence in pricing implementations. The barrier option and digital option examples have direct relevance to derivatives desk pricing.

The paper requires deep expertise in multiple advanced areas: Henstock-Kurzweil gauge integration, functional analysis (semigroup theory, strong continuity), stochastic calculus (Itô's lemma, Girsanov theorem), mathematical finance (Black-Scholes theory, risk-neutral pricing), and formal verification in Lean 4 / Mathlib. The Lean formalization involves proving Gaussian integral identities, semigroup properties, and closed-form solutions within a constructive type-theoretic framework. Reproducing the results requires setting up the Lean 4 / Mathlib environment and understanding the prior works in the series (HkPathIntegral.lean, HkFreeField.lean). The mathematical content itself is elegant but the formal verification layer adds substantial complexity.

The paper provides a complete Lean 4 / Mathlib formalization in the file HkBlackScholes.lean. All statements are sorry-free and depend only on the standard axioms propext, Classical.choice, and Quot.sound. The file imports HkPathIntegral.lean and HkFreeField.lean from earlier parts of the programme. Every theorem, lemma, and definition has a corresponding Lean name (e.g., black_scholes_call, Gdrift_semigroup, chernoff_step_eq). The mathematical proofs are self-contained with detailed proof sketches. The paper is the third in a series with prior works available via DOIs (10.5281/zenodo.21364715 and 10.5281/zenodo.21479996).