Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction
Abstract
We develop a machine-checked construction of non-Gaussian functional integrals using the Henstock--Kurzweil gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with action S(phi) = (1/2) phi^T A phi + lambda * sum_i phi_i^4, where A is positive definite. We prove that the one-mode integral I(omega, j, lambda) is finite, strictly positive, monotone and infinitely differentiable in the coupling lambda on [0, infinity). Its derivatives are given by convergent integrals of phi^{4k} with the same weight, not by the divergent perturbative series. The M-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff / Lie--Trotter splitting handles the non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 with Mathlib; the accompanying file HkNonGaussian.lean is free of sorry and uses only the standard axioms propext, Classical.choice, Quot.sound. Four illustrative applications are worked out at the level of explicit formulas: the Duffing oscillator, local volatility (CEV) in finance, Wilson--Cowan neural fields, and non-Gaussian quantum reservoirs. The construction is completely direct and does not use Wick rotation, Wiener measure, zeta-regularisation or analytic continuation back from imaginary time.
Related
- Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
- Gribov Copies and Gauge Invariance: A Henstock–Kurzweil Continuum Integral on the SU(3) Lattice
- A real-time path-integral framework for stochastic neural fields via the Henstock–Kurzweil integral and Külbs–Steadman spaces
- Gaussian Process Bandits for AI System Optimization with Selectively Verified Feedback
- Gaussian Integral Operator between Fock Spaces
BibTeX
@misc{berdinsky2026henstockkurzweil,
title = {{Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction}},
author = {Yuri N. Berdinsky},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.10793},
eprint = {2609.10793},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.10793},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction
AU - Yuri N. Berdinsky
PY - 2026
DA - 2026/09/09
PB - arXiv
DO - 10.48550/arxiv.2609.10793
UR - https://arxiv.org/abs/2609.10793
AB - We develop a machine-checked construction of non-Gaussian functional integrals using the Henstock--Kurzweil gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with action S(phi) = (1/2) phi^T A phi + lambda * sum_i phi_i^4, where A is positive definite. We prove that the one-mode integral I(omega, j, lambda) is finite, strictly positive, monotone and infinitely differentiable in the coupling lambda on [0, infinity). Its derivatives are given by convergent integrals of phi^{4k} with the same weight, not by the divergent perturbative series. The M-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff / Lie--Trotter splitting handles the non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 with Mathlib; the accompanying file HkNonGaussian.lean is free of sorry and uses only the standard axioms propext, Classical.choice, Quot.sound. Four illustrative applications are worked out at the level of explicit formulas: the Duffing oscillator, local volatility (CEV) in finance, Wilson--Cowan neural fields, and non-Gaussian quantum reservoirs. The construction is completely direct and does not use Wick rotation, Wiener measure, zeta-regularisation or analytic continuation back from imaginary time.
ER -