Henstock–Kurzweil Gauge Integral in the Non-Gaussian Regime: A Machine-Verified Construction

Author: Yuri N. Berdinsky, Saint Petersburg State University

Summary (Overview)

• The paper develops a rigorous mathematical framework for non-Gaussian functional integrals using the Henstock–Kurzweil (HK) gauge integral, avoiding the standard detours of Wick rotation, Wiener measure, ζ-regularisation, and analytic continuation.
• The central result concerns the one-mode quartic integral $I(\omega, j, \lambda) = \int_{\mathbb{R}} e^{-\frac{\omega}{2}\varphi^2 + j\varphi - \lambda\varphi^4} \mathcal{D}_{\mathrm{HK}}\varphi$, proven to be finite, strictly positive, monotone in $\lambda$, and $C^\infty$ in the coupling on $[0, \infty)$—despite having a divergent perturbative (Taylor) series.
• The $M$-mode influence functional is shown to factorise into one-mode integrals and is bounded above by its Gaussian value.
• A Chernoff/Lie–Trotter product formula handles the non-commutativity of free and non-Gaussian generators for bounded operators.
• All results are formally machine-checked in Lean 4 with Mathlib (file HkNonGaussian.lean), containing no sorry and using only standard axioms.

Introduction and Theoretical Foundation

Motivation: Beyond Gaussian Integrals

The paper begins with the fundamental finite-dimensional Gaussian integral, which underpins virtually all explicit computations in quantum field theory, statistical mechanics, and mathematical finance:

$$\int_{\mathbb{R}^n} e^{-\frac{1}{2}\varphi^T A \varphi} d^n\varphi = (2\pi)^{n/2}(\det A)^{-1/2}, \qquad A = A^T > 0. \tag{1}$$

When the action acquires a quartic self-interaction,

$$S(\varphi) = \frac{1}{2}\varphi^T A \varphi + \lambda \sum_{i=1}^{M} \varphi_i^4, \quad \lambda \geq 0, \tag{2}$$

the standard perturbative expansion $e^{-\lambda \sum_i \varphi_i^4} = \sum_k c_k \lambda^k$ has zero radius of convergence—it is purely asymptotic, with factorially growing coefficients.

The Classical Route (Five Analytic Detours)

The paper carefully recalls the standard physicist's approach to real-time path integrals:

1. Formal measure: The symbol $\mathcal{D}\varphi$ denotes "uniform measure on paths"—but Cameron's theorem shows no such countably additive complex measure exists on $C([0,t])$.
2. Wick rotation: Substitute $t \mapsto -i\tau$, turning $e^{iS/\hbar}$ into $e^{-S_E/\hbar}$ with Wiener measure $\mu_W$.
3. Cameron–Martin obstruction: Wiener measure is supported on nowhere-differentiable paths; the kinetic term $\int \dot{\varphi}^2$ is almost surely infinite.
4. ζ-regularisation: Define $\zeta_A(s) = \sum_k \mu_k^{-s}$ and $\det_\zeta A = \exp(-\zeta_A'(0))$ by analytic continuation.
5. Analytic continuation back to real time.

Each arrow is a nontrivial analytic step; Steps 2 and 5 are unavailable for general non-Gaussian actions with complex or time-dependent couplings.

The Gauge Route (Direct Construction)

The HK approach (developed for path integrals by Muldowney, and placed in the Kuelbs–Steadman framework by Gill–Zachary and Esposito–Gill) replaces this chain by a single real-time construction:

• Cylindrical intervals: Sets $\{\varphi : P\varphi \in J\}$ with $P$ a finite-rank projection and $J \subset \mathbb{R}^k$ a bounded interval.
• Gauge: A strictly positive function $\delta(\cdot) > 0$ on the space of tags.
• δ-fine partitions: Cells must be small in the sense prescribed by $\delta$ at their own tag.

The integral is the limit of Riemann sums over δ-fine partitions as the gauge is refined. Cousin's lemma guarantees δ-fine partitions exist for every gauge.

Methodology

Definitions

Definition 2.1 (Cylindrical interval): A set $I = \{\varphi \in \mathcal{H}: P\varphi \in J\}$ where $P: \mathcal{H} \to \mathbb{R}^k$ is a finite-rank orthogonal projection and $J = \prod_{r=1}^k (a_r, b_r] \subset \mathbb{R}^k$ is a bounded interval.

Definition 2.2 (Gauge and δ-fine partition): A gauge is $\delta: \mathcal{H} \to (0, \infty)$. A tagged partition $\{(\varphi_j, I_j)\}_{j \leq N}$ is δ-fine if each base is contained in the ball of radius $\delta(\varphi_j)$ around $P_j\varphi_j$.

Definition 2.3 (HK integral): A functional $F$ is HK-integrable with value $Z$ if for every $\varepsilon > 0$ there is a gauge $\delta$ such that

$$\left|\sum_j F(\varphi_j)\mu(I_j) - Z\right| < \varepsilon$$

for every δ-fine tagged partition.

Key Theorems

Theorem 2.5 (Gaussian gauge integral):

$$\int_{\mathbb{R}^n} e^{-\frac{1}{2}\varphi^T A \varphi} \mathcal{D}\varphi = \int_{\mathbb{R}^n} e^{-\frac{1}{2}\varphi^T A \varphi} \mathcal{D}_{\mathrm{HK}}\varphi = (2\pi)^{n/2}(\det A)^{-1/2}.$$

Theorem 3.1 (Existence and finiteness): For $\omega > 0$, $j \in \mathbb{R}$, $\lambda \geq 0$, $k \in \mathbb{N}$, the function $\varphi \mapsto \varphi^k e^{-\frac{\omega}{2}\varphi^2 + j\varphi - \lambda\varphi^4}$ is absolutely integrable. All moments

$$M_m(\omega, j, \lambda) = \int_{\mathbb{R}} \varphi^m e^{-\frac{\omega}{2}\varphi^2 + j\varphi - \lambda\varphi^4} d\varphi \tag{5}$$

are finite.

Proof sketch: Since $-\lambda\varphi^4 \leq 0$ and completing the square gives $-\frac{\omega}{2}\varphi^2 + j\varphi \leq \frac{j^2}{\omega} - \frac{\omega}{4}\varphi^2$, the weight is dominated by $e^{j^2/\omega}|\varphi|^k e^{-\frac{\omega}{4}\varphi^2}$, integrable against a Gaussian.

Proposition 3.2 (Positivity and monotonicity): For $0 \leq \lambda_1 \leq \lambda_2$:

$$0 < I(\omega, j, \lambda_2) \leq I(\omega, j, \lambda_1), \qquad I(\omega, j, 0) = \sqrt{\frac{2\pi}{\omega}} e^{j^2/(2\omega)}.$$

Theorem 3.3 (Differentiation under the integral sign) — the technical heart:

1. For every $\lambda > 0$ and $m \in \mathbb{N}$: $\frac{d}{d\lambda} M_m(\omega, j, \lambda) = -M_{m+4}(\omega, j, \lambda)$.
2. Consequently $\lambda \mapsto M_m(\omega, j, \lambda)$ is $C^\infty$ on $(0, \infty)$ with $\frac{d^k}{d\lambda^k} I(\omega, j, \lambda) = (-1)^k M_{4k}(\omega, j, \lambda)$.
3. At the boundary point $\lambda = 0$, the one-sided derivative exists:

$$\partial_\lambda I(\omega, j, 0) = -\int_{\mathbb{R}} \varphi^4 e^{-\frac{\omega}{2}\varphi^2 + j\varphi} d\varphi. \tag{6}$$

Proof of (1): Fix $\lambda > 0$, work on the ball $|\lambda' - \lambda| < \lambda/2$ where $\lambda' > \lambda/2$. The derivative is dominated uniformly by $(1+\varphi^{2m})\varphi^4 e^{-\frac{\omega}{2}\varphi^2 + j\varphi - \frac{\lambda}{2}\varphi^4}$, integrable by Theorem 3.1. Dominated convergence applies.

Proof of (3): The interior argument fails at $\lambda = 0$ (two-sided neighbourhoods contain negative couplings). Using $0 \leq e^{-u} - 1 + u \leq u^2$ for $u \geq 0$:

$$\left|\frac{I(\omega,j,\lambda) - I(\omega,j,0)}{\lambda} + M_4(\omega,j,0)\right| \leq \lambda M_8(\omega,j,0) \xrightarrow[\lambda \downarrow 0]{} 0.$$

Example 3.5: For $j=0$, $\omega=1$: $M_4(1,0,0) = 3\sqrt{2\pi}$, hence

$$I(1,0,\lambda) = \sqrt{2\pi}(1 - 3\lambda + O(\lambda^2)), \quad \lambda \downarrow 0$$

with remainder controlled by $\lambda^2 M_8(1,0,0) = 105\sqrt{2\pi}\lambda^2$.

M-Mode Results

Theorem 4.1 (Factorisation): In the eigenmode basis,

$$\mathcal{F}_\lambda(j) = \prod_{i=1}^{M} I(\omega_i, j_i, \lambda).$$

Theorem 4.2 (Bounds and smoothness):

$$0 < \mathcal{F}_\lambda(j) \leq \mathcal{F}_0(j) = (2\pi)^{M/2}(\det A)^{-1/2} e^{\frac{1}{2}j^T A^{-1} j},$$

and $\lambda \mapsto \mathcal{F}_\lambda(j)$ is $C^\infty$ on $(0, \infty)$ with one-sided derivatives at $0$.

Chernoff Splitting

Theorem 5.2 (Strong Chernoff/Lie–Trotter splitting): For $A_0, B_\lambda \in \mathcal{B}(\mathcal{H})$ (bounded operators on a complex Hilbert space), for every $\psi \in \mathcal{H}$ and $t \in \mathbb{R}$:

$$\left(e^{tA_0/N} e^{tB_\lambda/N}\right)^N \psi \xrightarrow[N \to \infty]{} e^{t(A_0 + B_\lambda)} \psi.$$

The proof shows $F_\lambda(t) = e^{tA_0}e^{tB_\lambda}$ is a Chernoff family ($F_\lambda(0) = \mathbf{1}$, $F_\lambda'(0) = A_0 + B_\lambda$) and applies the norm-topology Chernoff theorem.

Empirical Validation / Results

Machine Verification (Lean 4)

The formal development uses Mathlib with six files:

Verification status: The file compiles without errors, contains no occurrence of sorry or admit, introduces no axioms of its own, and depends only on the three standard Lean kernel axioms (propext, Classical.choice, Quot.sound).

Representative Lean Excerpts

def oneModeWeight (om j lam x : R) : R := 
  Real.exp(-(om / 2) * x ^ 2 + j * x - lam * x ^ 4)

def nonGaussianOneModeIntegral (om j lam : R) : R := 
  ∫ x : R, oneModeWeight om j lam x

theorem nonGaussianOneModeFinite (om j lam : R) (hom : 0 < om) (hlam : 0 ≤ lam) : 
  Integrable (oneModeWeight om j lam)

theorem nonGaussianOneModeDifferentiable (om j : R) (hom : 0 < om) {lam : R} (hlam : 0 ≤ lam) :
  HasDerivWithinAt (fun l => nonGaussianOneModeIntegral om j l)
    (-oneModeMoment om j lam 4) (Ici 0) lam

Four Illustrative Applications

1. Duffing oscillator: $\ddot{x} + \gamma\dot{x} + x + 4\lambda x^3 = \sqrt{2\gamma T}\xi(t)$ has stationary distribution $p(x) \propto e^{-\frac{1}{T}(x^2/2 + \lambda x^4)}$. The first anharmonic correction to the variance is $\partial_\lambda\langle x^2\rangle|_0 = -12T^3$ (variance reduction for a stiffening spring).

2. Local volatility (CEV) in finance: Replacing constant $\sigma$ by $\sigma(x) = \sigma_0 + \varepsilon f(x)$ produces a quartic weight with $\lambda \propto \varepsilon^2$. The first-order smile correction is $\partial_\lambda \log \mathcal{F}_\lambda(j)|_{\lambda=0} = -\sum_i \frac{M_4(\omega_i, j_i, 0)}{M_0(\omega_i, j_i, 0)}$, a convergent expression.

3. Wilson–Cowan neural fields: The sigmoidal transfer function $S(\varphi) \approx \varphi - \frac{1}{6}\varphi^3$ generates a $-\frac{1}{3}\varphi^4$ term in the effective action, i.e., $\lambda = \frac{1}{3}$.

4. Non-Gaussian quantum reservoirs: A two-level system coupled to $M$ anharmonic modes with Hamiltonian $H = H_S + \sum_i(\frac{p_i^2}{2} + \frac{\omega_i^2}{2}q_i^2 + \lambda q_i^4) + \sigma_z \sum_i g_i q_i$. Theorem 4.2 guarantees finite decoherence rates bounded by the harmonic case.

Theoretical and Practical Implications

Key Conceptual Insight

The paper's central message: the failure of perturbative series is a failure of method, not of the object. The map $\lambda \mapsto I(\omega, j, \lambda)$ is not analytic at $\lambda = 0$ (its formal Taylor series diverges for every $\lambda \neq 0$), yet it is $C^\infty$ on $[0, \infty)$ in the sense of one-sided derivatives. Smoothness and analyticity are different notions, and only the first is needed for physics.

The theorem produces the numbers $\partial_\lambda^k I$ but makes no claim that $\sum_k \partial_\lambda^k I(0)\lambda^k/k!$ converges—it does not. What one obtains is a $C^\infty$ function with prescribed derivatives, i.e., exactly the information that Borel summation or rigorous asymptotic analysis needs as input.

Practical Advantages

• Direct real-time construction: No Wick rotation, no Wiener measure, no ζ-regularisation, no analytic continuation.
• Compatibility with Lebesgue: For absolutely convergent integrands (all those in Sections 3–4), the gauge value equals the Lebesgue value—which is why the Lean formalisation uses Mathlib's Bochner integral without loss of rigour.
• Machine verification: All four main statements (A)–(D) are formally verified, providing unprecedented reliability.

Conclusion

The Henstock–Kurzweil gauge integral combined with Chernoff product approximations provides a rigorous, machine-verified route to non-Gaussian functional integrals for finitely many bosonic modes. The resulting integrals are finite, positive, factorising, and smooth in the coupling—with smoothness obtained by differentiation under the integral sign rather than by a divergent perturbative series.

Future Directions

1. Continuum limit: Passing from $M$ modes to a field requires uniform control of constants in Theorem 4.2 as $M \to \infty$, with the ζ-regularised determinant reappearing as the limit of finite products.
2. Fermionic analogue: Grassmann variables have no positivity, but their integrals are finite sums; a gauge formulation combining both sectors would cover supersymmetric models.
3. Complex couplings: For $\lambda \in \mathbb{C}$ with $\text{Re}\,\lambda \geq 0$, the HK integral is natural since absolute integrability is not required.
4. Fully non-perturbative regimes: Instanton-dominated situations make the smoothness-vs-analyticity distinction physically visible.

The strong Chernoff theorem is formulated for abstract complex Hilbert spaces without finite-dimensionality assumptions, so the principal barrier to the continuum limit lies in constructing an infinite-dimensional cylindrical HK measure and proving existence of the non-absolutely convergent limit of $\mathcal{F}_\lambda(j)$ as $M \to \infty$—for which the present finite-dimensional theory supplies all necessary projective bounds.