{"id":"arxiv/2610.37346","url":"https://arxiv.org/abs/2610.37346","tags":["math-ph"],"score":0,"title":"Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4","domain":"math-ph","source":"arxiv","authors":["Yu. N. Berdinsky"],"reviews":0,"subject":"math-ph","summary":"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 $\\mathbb{R}^k$ is identified with the standard Gaussian one. Third, the Saks-Henstock lemma and additivity are proved. Fourth, the Fresnel formula $\\int_{\\mathbb{R}} e^{i a x^2/2} dx = \\sqrt{2π/a} e^{iπ/4}$ is proved as an improper (gauge) integral. This yields the projective consistency of the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-27","reactions":{}}