Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
Yu. N. Berdinsky
math-ph
Oct 27, 2026 · v1
TL;DR
Formalizes in Lean 4 on Mathlib the Henstock–Kurzweil free-field Feynman integral, the Fresnel formula, the generating functional and Wick's theorem, with no sorry and no new axioms.
Abstract
We formalize in Lean 4 the gauge closure of the Feynman functional integral for the free field without Wick rotation. First, the restriction to box divisions is removed via a direction bound and a uniform Riemann-sum estimate for all $δ$-fine cylindrical divisions. Second, the coordinate measure on $\mathbb{R}^k$ is identified with the standard Gaussian one. Third, the Saks-Henstock lemma and additivity are proved. Fourth, the Fresnel formula $\int_{\mathbb{R}} e^{i a x^2/2} dx = \sqrt{2π/a} e^{iπ/4}$ is proved as an improper (gauge) integral. This yields the projective consistency of the oscillating Gaussian premeasure and the existence of the free-field integral. The free field is completely closed: we prove the Fresnel formula for an arbitrary symmetric positive-definite action $A$, compute the generating functional and the two-point function $\langle y_p y_q \rangle = i(A^{-1})_{pq}$, and prove Wick's theorem. The interacting field $λ\varphi^4$, unbounded generators, and renormalisation remain open. All results are machine-verified with no sorry or new axioms.
Problem
The Feynman functional integral for the free field is only conditionally convergent, so the Lebesgue integral is undefined without Wick rotation. Earlier stages of the programme proved consistency only for divisions into cylinders over boxes with a single direction space.
Approach
The Henstock–Kurzweil (gauge) integral on Kuelbs–Steadman spaces is extended in Lean 4 on Mathlib. A direction bound removes the restriction to box divisions, and the coordinate Gaussian measure is identified with the standard Gaussian on R^k. The Saks–Henstock lemma and additivity are then proved, and the Fresnel formula is established as an improper gauge integral. Non-diagonal actions are handled by orthogonal diagonalisation with eigenbasis-adapted exhausting cubes.
Results
The oscillating Gaussian premeasure is shown to be projectively consistent, and the free-field integral is shown to exist. Also proved are the Fresnel formula for any symmetric positive-definite action, the generating functional, the two-point function i(A^{-1})_{pq}, and Wick's theorem for all n-point functions. Everything is machine-checked with no sorry or new axioms; the interacting field, unbounded generators and renormalisation remain open.
