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

技术摘要：费曼预测度的代数完备性

问题陈述
本研究旨在通过不使用 Wick 旋转（即保持在实时间内）的方法，对无限维自由场的费曼泛函积分进行严格构建。主要的挑战在于定义振荡核 $e^{iS(\phi)}$ 的积分，由于其被积函数的模恒等于 1，导致勒贝格积分无法定义。作者程序的前期阶段已在 Kuelbs–Steadman 空间上建立了 Henstock–Kurzweil (HK) 路径积分，针对特定情况，但留下了四个尚未解决的具体“未来目标”：

1. 取消对一致性定理中“盒划分”（box divisions）的限制，允许任意柱状划分（cylindrical divisions）。
2. 严格识别坐标诱导的高斯测度与 $\mathbb{R}^k$ 上的标准高斯密度。
3. 证明 Saks–Henstock 引理、对任意有限分解的加法性，以及使用不同模数（$V_n$ 与 $V_m$）描述之间的一致性。
4. 通过 Fresnel 公式建立自由场泛函积分的存在性，且无需 Wick 旋转。

此外，本文旨在在所有相关函数（Wick 定理）层面完成自由场的描述，并将该振荡预测度嵌入到一般的柱状预测度理论中。

方法论
这项工作是一个基于 Lean 4 在 Mathlib 库之上的形式化验证项目。其方法论依赖于 Henstock–Kurzweil（测度/规范）积分，该积分推广了 Riemann 积分，能够处理那些因不满足绝对收敛而导致失效的条件收敛振荡积分。

关键方法论组件包括：

• 柱状单元的几何分析： 证明任何包含在有界盒之上的非空柱状单元都必须约束所有坐标方向（定理 3.1）。这种“方向界限”使得在任意柱状划分（而非仅限于对齐子盒的划分）上进行一致的 Riemann 和估计成为可能。
• Abelian 正则化： 本文并非利用 Wick 旋转（将时间旋转到复平面），而是利用 Abelian 正则化参数 $\varepsilon \to 0^+$ 来处理振荡核 $e^{iax^2/2}$。这涉及证明即使在阻尼参数的实部为零时仍然成立的一致尾部估计（定理 6.1）。
• 谱分解： 对于非对角作用量，论文采用正定作用量矩阵 $A$ 的正交对角化，将积分转化为一维 Fresnel 积分的乘积，并利用与特征基对齐的适配立方体。
• 生成泛函： 相关函数不是通过直接积分无界多项式（这需要单独的收敛性分析）得到的，而是通过对来自 Fresnel 公式的闭合形式生成泛函 $Z(j)$ 进行求导得到的。
• 形式化验证： 每一个定理都经过了机器检查。形式化过程避免了除 propext、Classical.choice 和 Quot.sound 之外的公理，并且不包含任何 sorry 或 admit 语句。

主要贡献与结果

1. 任意柱状划分 (目标 8.1)：
   本文证明了 HK 积分对于任意柱状划分是一致的，消除了此前对子盒划分的限制。一个“方向界限”定理确保了规范（gauge）能够控制任何单元的坐标，从而实现一致的 Riemann 和估计（定理 3.3）。

2. 高斯测度的识别 (目标 8.2)：
   形式化证明了 $\mathbb{R}^k$ 上坐标泛函诱导的测度正是具有密度 $(2\pi)^{-k/2}e^{-|y|^2/2}$ 的标准高斯测度（定理 4.1）。

3. Saks–Henstock 与加法性 (目标 8.3)：
   在柱状设置下建立了 Saks–Henstock 引理，证明了在 $\delta$-精细偏系统上的绝对误差之和是有界的。由此导出了积分在任意有限分解下的加法性，以及使用不同模数（$n$ 与 $m$）描述柱状体时积分值的相容性（定理 5.4）。

4. Fresnel 公式与自由场 (目标 8.4)：

   • 一维 Fresnel 公式： 证明了极限 $\lim_{R\to\infty} \int_{-R}^R e^{iax^2/2} dx = \sqrt{2\pi/a} e^{i\pi/4}$ 是一个不需要 Wick 旋转的广义规范积分（定理 6.2）。
   • 多维扩展： 利用正交对角化和适配立方体，将此结论扩展到任意对称正定作用量 $A$（定理 7.2）。
   • 存在性： 证明了自由场 $e^{iS(\phi)}$ 在任何有界盒之上的柱状体上是 HK 可积的（定理 6.5）。

5. 生成泛函与相关函数：

   • 构建了一个带有外部源的生成泛函 $Z(j)$，得到 $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)$（定理 7.3）。
   • 计算了两点函数为 $\langle y_p y_q \rangle = i(A^{-1})_{pq}$（定理 7.4）。
   • Wick 定理： 证明了奇数阶相关函数消失，且偶数阶相关函数分解为两点函数的配对之和（定理 8.6）。四点函数被显式导出，展示了特征性的实时间因子 $i$（推论 8.7）。

6. 一般理论与极限：

   • 该振荡预测度被作为复柱状预测度嵌入到一般理论中，并证明了其投影一致性（定理 9.2）。
   • HK 积分的值被识别为 Fresnel 值（定理 9.3）。
   • 建立了从阻尼（欧几里得）高斯预测度到振荡预测度的过渡，将其确立为 $\varepsilon \to 0^+$ 的极限，从而在不进行轮廓旋转的情况下确认了两者之间的联系（定理 11.1）。

7. 在金融数学中的应用：
   作为该机制（特别是高斯尾部恒等式和 HK 一致性）的演示，本文将欧式看涨期权的 Black–Scholes 公式推导为一个 Henstock–Kurzweil 积分。该推导依赖于高斯柱状预测度，并简化为一维高斯尾部计算，完全避免了 Wick 旋转（第 10 节）。

意义与主张
本文声称实现了 Henstock–Kurzweil 框架下自由场费曼预测度的代数完备性。具体而言：

• 它提供了一个经机器验证的证明，证明了自由场泛函积分的存在性及其等于 Fresnel 值，且无需调用 Wick 旋转。
• 它通过 Wick 定理，在所有相关函数层面（而非仅仅是两点函数）完成了对自由场的描述。
• 它建立了振荡预测度的投影一致性，使其可以作为一般的柱状预测度理论中的严格对象进行处理。
• 它证明了可以使用 Abelian 正则化和规范积分来严格处理“实时间”振荡积分，这与欧几里得（阻尼）方法截然不同。

范围与局限性
作者明确指出，本工作仅限于自由场。以下内容仍是未来工作的开放问题：

• 相互作用场（特别是无限模数下的 $\lambda \phi^4$）。
• 无界生成元（需要 Trotter–Kato 或 $C_0$-半群）。
• 重整化与构造量子场论。
• 规范场论的连续极限（尽管相关装置已应用于另一篇论文中的 Gribov 复制）。

论文强调，其贡献在于在机器验证的形式下完成了自由场情况的严格闭合，为未来的扩展（如非高斯领域、Chernoff–Lie–Trotter 方案）提供了必要的组件，但并未亲自执行这些扩展。