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

技術要約：ファインマン前測度の代数的完備性

問題提起
本研究は、ウィック回転（すなわち実時間での記述）を用いずに、無限次元における自由場のファインマン汎関数積分を厳密に構成することを目的としている。主要な課題は、被積分関数の絶対値が恒等的に1であるため、ルベーグ積分が定義不可能な振動核 $e^{iS(\phi)}$ の積分を定義することにある。著者のプログラムの以前の段階では、特定のケースにおいてクエルブ・ステッドマン空間上のヘンストック–クルツヴェイル（HK）経路積分を確立したが、以下の4つの具体的な「将来の目標」が未解決のまま残されていた：

1. 一貫性定理における「ボックス分割」への制限を排除し、任意の円筒分割を許容すること。
2. 座標誘導によるガウス測度を、標準的な $\mathbb{R}^k$ 上のガウス密度と厳密に同一視すること。
3. サックス–ヘンストックの補題、任意の有限分解に対する加法性、および異なるモード数（$V_n$ 対 $V_m$）を用いた記述間の整合性の証明。
4. ウィック回転を用いずに、フレネル公式を通じて自由場汎関数積分の存在を確立すること。

さらに、本論文は、すべての相関関数（ウィックの定理）のレベルで自由場の記述を完結させ、振動前測度を円筒前測度の一般理論へと埋め込むことを目指している。

方法論
本研究は、Lean 4 を用い、Mathlib ライブラリ上で実装された形式検証プロジェクトである。手法としては、リーマン積分を一般化し、絶対収束しない条件付き収束的な振動積分を扱うことが可能なヘンストック–クルツヴェイル（ゲージ）積分に依拠している。

主な方法論的構成要素は以下の通りである：

• 円筒の幾何学的解析： 有界なボックス上の円筒に含まれる空でない円筒セルは、すべての座標方向を拘束することを証明する（定理3.1）。この「方向の拘束」により、単純な部分ボックスに整列したものだけでなく、任意の円筒分割に対して一様なリーマン和の推定が可能となる。
• アベリアン正則化： ウィック回転（時間を複素平面へ回転させる手法）の代わりに、振動核 $e^{iax^2/2}$ を扱うためにアベリアン正則化パラメータ $\varepsilon \to 0^+$ を利用する。これには、減衰パラメータの実部がゼロの場合でも成立する一様なテイル推定（定理6.1）の証明が含まれる。
• スペクトル分解： 非対角のアクションに対しては、正定値アクション行列 $A$ の直交対角化を用いて、積分を1次元フレネル積分の積へと変換し、固有基底に適合した立方体を利用する。
• 生成汎関数： 相関関数は、非有界な多項式の直接積分（これは別途収束解析を必要とする）によってではなく、フレネル公式から得られる閉形式の生成汎関数 $Z(j)$ を微分することによって導出される。
• 形式検証： すべての定理は機械的にチェックされている。この形式化は propext, Classical.choice, Quot.sound 以外の公理を使用せず、sorry や admit 文を含まない。

主な貢献および結果

1. 任意の円筒分割 (目標 8.1):
   本論文は、HK積分が任意の円筒分割に対して一貫していることを証明し、以前の「部分ボックス上の分割」という制限を排除した。「方向の拘束」定理により、ゲージがセルの座標を制御することが保証され、一様なリーマン和の推定が可能となる（定理3.3）。

2. ガウス測度の同一視 (目標 8.2):
   $\mathbb{R}^k$ 上の座標汎関数によって誘導される測度が、密度 $(2\pi)^{-k/2}e^{-|y|^2/2}$ を持つ標準ガウス測度と完全に一致することを形式的に証明した（定理4.1）。

3. サックス–ヘンストックと加法性 (目標 8.3):
   円筒の設定においてサックス–ヘンストックの補題を確立し、$\delta$-細かい部分系における絶対誤差の和が有界であることを示した。これにより、任意の有限分解に対する積分の加法性と、円筒を記述するために使用されるモード数（$n$ 対 $m$）に関わらず積分の値が一貫していることが示される（定理5.4）。

4. フレネル公式と自由場 (目標 8.4):

• 1次元フレネル公式： ウィック回転を用いずに、$\lim_{R\to\infty} \int_{-R}^R e^{iax^2/2} dx = \sqrt{2\pi/a} e^{i\pi/4}$ が不適切ゲージ積分として成立することを証明した（定理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）。
• 2点関数は $\langle y_p y_q \rangle = i(A^{-1})_{pq}$ として計算される（定理7.4）。
• ウィックの定理： 奇数次の相関関数は消失し、偶数次の相関関数は2点関数のペアリングの和へと因子分解されることが証明された（定理8.6）。4点関数は明示的に導出され、特徴的な実時間因子 $i$ を示す（系8.7）。

6. 一般理論と極限:

• 振動前測度は、複素円筒前測度として一般理論へと埋め込まれ、その射影的一貫性が証明された（定理9.2）。
• HK積分の値はフレネル値と一致すると特定された（定理9.3）。
• 減衰した（ユークリッド）ガウス前測度から振動前測度への移行は、$\varepsilon \to 0^+$ の極限として確立され、輪郭回転なしに両者の関係が確認された（定理11.1）。

7. 金融数学への応用:
   （特にガウスのテイル恒等式とHKの一貫性に焦点を当てた）機械のデモンストレーションとして、欧州型コールオプションのブラック・ショールズ公式をヘンストック–クルツヴェイル積分として導出している。この導出は、ガウス円筒前測度に依拠しており、ウィック回転を一切用いずに1次元のガウス・テイル計算へと帰着される（セクション10）。

意義および主張
本論文は、ヘンストック–クルツヴェイルの枠組みにおける自由場のファインマン前測度の代数的完備性を達成したと主張している。具体的には：

• 自由場汎関数積分が存在し、それがフレネル値に等しいことを、ウィック回転を呼び出すことなく機械検証された形で証明した。
• 2点関数だけでなく、ウィックの定理を通じて、自由場の記述をすべての相関関数のレベルで完結させた。
• 振動前測度の射影的一貫性を確立し、それを一般の円筒前測度理論における厳密な対象として扱うことを可能にした。
• 「実時間」の振動積分が、アベリアン正則化とゲージ積分を用いることで、ユークリッド的（減衰した）アプローチとは異なる形で厳密に扱えることを示した。

範囲と限界
著者は、本研究の範囲が自由場に限定されていることを明示している。以下の事項は今後の課題として残されている：

• 相互作用のある場（特に無限モードにおける $\lambda \phi^4$）。
• 非有界な生成子（トロッター–カトまたは $C_0$-半群を必要とするもの）。
• 再正規化および構成的量子場理論。
• ゲージ理論の連続極限（ただし、関連論文においてゴロフ・コピーへの適用については言及されている）。

本論文は、自身の貢献が自由場ケースの機械検証された形での厳密な終結であり、将来の拡張（非ガウス領域やチェンノフ–リー–トロッター・スキームなど）に必要な材料を提供することにあると強調している。