Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
Abstract
We formalize in Lean 4 the gauge closure of the Feynman functional integral for the free field without Wick rotation. First, the restriction to box divisions is removed via a direction bound and a uniform Riemann-sum estimate for all δ-fine cylindrical divisions. Second, the coordinate measure on ℝk is identified with the standard Gaussian one. Third, the Saks-Henstock lemma and additivity are proved. Fourth, the Fresnel formula ∫ℝ ei a x2/2 dx = √(2π/a) eiπ/4 is proved as an improper (gauge) integral. This yields the projective consistency of the oscillating Gaussian premeasure and the existence of the free-field integral. The free field is completely closed: we prove the Fresnel formula for an arbitrary symmetric positive-definite action A, compute the generating functional and the two-point function ⟨ yp yq ⟩ = i(A−1)pq, and prove Wick's theorem. The interacting field λφ4, unbounded generators, and renormalisation remain open. All results are machine-verified with no sorry or new axioms.
Related
- Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction
- 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
- Algebraic Proof of Completeness of a Positional Numeral System in the Normalized Mersenne Basis
- Tense Logic via Truth Degrees: An Algebraic Completeness Result for Kashima's Calculus
BibTeX
@misc{berdinsky2026algebraic,
title = {{Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4}},
author = {Yu. N. Berdinsky},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.37346},
eprint = {2610.37346},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.37346},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
AU - Yu. N. Berdinsky
PY - 2026
DA - 2026/10/27
PB - arXiv
DO - 10.48550/arxiv.2610.37346
UR - https://arxiv.org/abs/2610.37346
AB - We formalize in Lean 4 the gauge closure of the Feynman functional integral for the free field without Wick rotation. First, the restriction to box divisions is removed via a direction bound and a uniform Riemann-sum estimate for all δ-fine cylindrical divisions. Second, the coordinate measure on ℝ^k is identified with the standard Gaussian one. Third, the Saks-Henstock lemma and additivity are proved. Fourth, the Fresnel formula ∫_ℝ e^i a x^2/2 dx = √(2π/a) e^iπ/4 is proved as an improper (gauge) integral. This yields the projective consistency of the oscillating Gaussian premeasure and the existence of the free-field integral. The free field is completely closed: we prove the Fresnel formula for an arbitrary symmetric positive-definite action A, compute the generating functional and the two-point function ⟨ y_p y_q ⟩ = i(A^−1)_pq, and prove Wick's theorem. The interacting field λφ^4, unbounded generators, and renormalisation remain open. All results are machine-verified with no sorry or new axioms.
ER -