Henstock--Kurzweil 规范积分在非高斯体系中的应用：一种机器验证的构造
Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction
- Saint Petersburg State University（圣彼得堡国立大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文用 Henstock--Kurzweil 积分和 Chernoff 近似构造非高斯泛函积分，在 Lean 4 中验证，并给出四个应用示例。
AI中文摘要：
我们利用 Henstock--Kurzweil 规范积分和 Chernoff 乘积近似，开发了一种机器验证的非高斯泛函积分构造。核心对象是一个有限的玻色子模式族，其作用量为 S(phi) = (1/2) phi^T A phi + lambda * sum_i phi_i^4，其中 A 是正定的。我们证明了单模积分 I(omega, j, lambda) 在耦合常数 lambda 属于 [0, infinity) 时是有限的、严格正的、单调的，并且关于 lambda 无穷可微。其导数由具有相同权重的 phi^{4k} 的收敛积分给出，而非发散的微扰级数。M 模影响泛函可分解为单模积分的乘积，并且以其高斯值为界。Chernoff / Lie--Trotter 分裂处理了自由生成元和非高斯生成元的非对易性。所有陈述均在 Lean 4 和 Mathlib 中形式化；随附文件 this http URL 没有 sorry，并且仅使用标准公理 propext、this http URL、this http URL。四个示例应用在显式公式层面得到解决：Duffing 振子、金融中的局部波动率 (CEV)、Wilson--Cowan 神经场以及非高斯量子储层。该构造完全直接，不使用 Wick 旋转、Wiener 测度、zeta 正则化或从虚时解析延拓。
英文摘要：
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.
