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

This preprint develops a rigorous, machine-checked construction of non-Gaussian functional integrals using the Henstock–Kurzweil (HK) gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with an action containing a quartic self-interaction λ∑iφi4λ∑iφi4. We show that the one-mode non-Gaussian integral is finite, positive, monotone and infinitely differentiable in the coupling λλ on [0,∞)[0,∞), with derivatives given by convergent integrals rather than by the divergent perturbative series. The MM-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff/Lie–Trotter splitting handles non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 / Mathlib and are free of sorry, using only the standard axioms propext, Classical.choice, Quot.sound. The accompanying Lean file HkNonGaussian.lean is included. 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. This work is a direct continuation of the author’s programme on machine-verified path integrals without Wick rotation.