Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4

Technical Summary: Algebraic Completeness of Feynman Premeasures

Problem Statement
This work addresses the rigorous construction of the Feynman functional integral for the free field in infinite dimensions without employing Wick rotation (i.e., remaining in real time). The primary challenge lies in defining the integral of the oscillating kernel $e^{iS(\phi)}$, where the modulus of the integrand is identically one, rendering the Lebesgue integral undefined. Previous stages of the author's program established the Henstock–Kurzweil (HK) path integral on Kuelbs–Steadman spaces for specific cases, but left four specific "future goals" unresolved:

1. Removing the restriction to "box divisions" in consistency theorems, allowing for arbitrary cylindrical divisions.
2. Rigorously identifying the coordinate-induced Gaussian measure with the standard Gaussian density on $\mathbb{R}^k$.
3. Proving the Saks–Henstock lemma, additivity over arbitrary finite decompositions, and consistency between descriptions using different numbers of modes ($V_n$ vs. $V_m$).
4. Establishing the existence of the free-field functional integral via the Fresnel formula without Wick rotation.

Furthermore, the paper seeks to close the description of the free field at the level of all correlation functions (Wick's theorem) and embed the oscillating premeasure into the general theory of cylindrical premeasures.

Methodology
The work is a formal verification project implemented in Lean 4 on top of the Mathlib library. The methodology relies on the Henstock–Kurzweil (gauge) integral, which generalizes the Riemann integral and is capable of handling conditionally convergent oscillatory integrals that fail absolute convergence.

Key methodological components include:

• Geometric Analysis of Cylinders: Proving that any nonempty cylindrical cell contained within a cylinder over a bounded box must constrain all coordinate directions (Theorem 3.1). This "direction bound" allows for uniform Riemann-sum estimates over arbitrary cylindrical divisions, not just those aligned with sub-boxes.
• Abelian Regularization: Instead of Wick rotation (rotating time to the complex plane), the proofs utilize an Abelian regularization parameter $\varepsilon \to 0^+$ to handle the oscillating kernel $e^{iax^2/2}$. This involves proving uniform tail estimates (Theorem 6.1) that hold even when the real part of the damping parameter is zero.
• Spectral Decomposition: For non-diagonal actions, the paper employs orthogonal diagonalization of the positive-definite action matrix $A$ to transform the integral into a product of one-dimensional Fresnel integrals, utilizing adapted cubes aligned with the eigenbasis.
• Generating Functionals: Correlation functions are derived not by direct integration of unbounded polynomials (which would require separate convergence analysis), but by differentiating the closed-form generating functional $Z(j)$ obtained from the Fresnel formula.
• Formal Verification: Every theorem is machine-checked. The formalization avoids axioms beyond propext, Classical.choice, and Quot.sound, and contains no sorry or admit statements.

Key Contributions and Results

1. Arbitrary Cylindrical Divisions (Goal 8.1):
   The paper proves that the HK integral is consistent for arbitrary cylindrical divisions, removing the previous restriction to divisions over sub-boxes. A "direction bound" theorem ensures that the gauge controls the coordinates of any cell, enabling a uniform Riemann-sum estimate (Theorem 3.3).

2. Identification of Gaussian Measures (Goal 8.2):
   It is formally proven that the measure induced by coordinate functionals on $\mathbb{R}^k$ is exactly the standard Gaussian measure with density $(2\pi)^{-k/2}e^{-|y|^2/2}$ (Theorem 4.1).

3. Saks–Henstock and Additivity (Goal 8.3):
   The Saks–Henstock lemma is established in the cylindrical setting, proving that the sum of absolute errors over a $\delta$-fine partial system is bounded. This leads to the additivity of the integral over arbitrary finite decompositions and the consistency of integral values regardless of the number of modes ($n$ vs. $m$) used to describe the cylinder (Theorem 5.4).

4. The Fresnel Formula and Free Field (Goal 8.4):

   • One-Dimensional Fresnel Formula: The limit $\lim_{R\to\infty} \int_{-R}^R e^{iax^2/2} dx = \sqrt{2\pi/a} e^{i\pi/4}$ is proven as an improper gauge integral without Wick rotation (Theorem 6.2).
   • Multi-dimensional Extension: This is extended to arbitrary symmetric positive-definite actions $A$ using orthogonal diagonalization and adapted cubes (Theorem 7.2).
   • Existence: The free-field functional $e^{iS(\phi)}$ is proven to be HK-integrable on any cylinder over a bounded box (Theorem 6.5).

5. Generating Functional and Correlation Functions:

   • A generating functional $Z(j)$ with an external source is constructed, yielding the value $Z(j) = (2\pi)^{k/2} e^{i\pi k/4} (\det A)^{-1/2} \exp(-\frac{i}{2}\langle j, A^{-1}j \rangle)$ (Theorem 7.3).
   • The two-point function is computed as $\langle y_p y_q \rangle = i(A^{-1})_{pq}$ (Theorem 7.4).
   • Wick's Theorem: It is proven that odd-order correlations vanish and even-order correlations factorize into sums over pairings of the two-point function (Theorem 8.6). The four-point function is explicitly derived, showing the characteristic real-time factor of $i$ (Corollary 8.7).

6. General Theory and Limits:

   • The oscillating premeasure is embedded into the general theory as a complex cylindrical premeasure, and its projective consistency is proven (Theorem 9.2).
   • The value of the HK integral is identified with the Fresnel value (Theorem 9.3).
   • The passage from damped (Euclidean) Gaussian premeasures to the oscillating one is established as the limit $\varepsilon \to 0^+$, confirming the link between the two pictures without contour rotation (Theorem 11.1).

7. Application to Financial Mathematics:
   As a demonstration of the machinery (specifically the Gaussian tail identities and HK consistency), the paper derives the Black–Scholes formula for a European call option as a Henstock–Kurzweil integral. This derivation relies on the Gaussian cylindrical premeasure and reduces to a one-dimensional Gaussian tail calculation, avoiding Wick rotation entirely (Section 10).

Significance and Claims
The paper claims to achieve the algebraic completeness of the Feynman premeasure for the free field within the Henstock–Kurzweil framework. Specifically:

• It provides a machine-verified proof that the free-field functional integral exists and equals the Fresnel value without invoking Wick rotation.
• It closes the description of the free field at the level of all correlation functions via Wick's theorem, not just the two-point function.
• It establishes the projective consistency of the oscillating premeasure, allowing it to be treated as a rigorous object within the general theory of cylindrical premeasures.
• It demonstrates that the "real-time" oscillating integral can be handled rigorously using Abelian regularization and gauge integration, distinct from the Euclidean (damped) approach.

Scope and Limitations
The author explicitly states that the work is delimited to the free field. The following remain open problems for future work:

• Interacting fields (specifically $\lambda \phi^4$ in infinitely many modes).
• Unbounded generators (requiring Trotter–Kato or $C_0$-semigroups).
• Renormalization and constructive Quantum Field Theory.
• The continuum limit of gauge theories (though the apparatus is applied to Gribov copies in a companion paper).

The paper emphasizes that its contribution is the rigorous closure of the free-field case in machine-verified form, providing the necessary ingredients (non-Gaussian regimes, Chernoff–Lie–Trotter schemes) for future extensions but not performing them itself.