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

Abstract

This work brings the gauge closure of the Feynman functional integral for the free field, without Wick rotation, into machine-verified form. First, the restriction to box divisions of cylinders is removed: a direction bound is proved, showing that every nonempty cylindrical cell contained in a cylinder over a bounded box must constrain all coordinate directions; from it a uniform Riemann-sum estimate is obtained, valid for all δ-fine divisions into arbitrary cylindrical cells. Second, the measure induced by the coordinate functionals on R^k is identified with the standard Gaussian measure with density (2π)^(−k/2) exp(−|y|²/2). Third, the Saks–Henstock lemma is proved in the cylindrical setting, together with additivity of the integral over arbitrary finite decompositions of a cylinder and the consistency of the descriptions of one and the same cylinder in terms of V_n and V_m for n ≤ m. Fourth, the Fresnel formula ∫R e^{iax²/2} dx = √(2π/a) e^{iπ/4} is proved as an improper (gauge) integral — the key analytic fact which is inaccessible to the Lebesgue integral — and from it the projective consistency of the oscillating Gaussian premeasure, the existence of the free-field functional integral as a Henstock–Kurzweil integral on every cylinder over a bounded box, and the finite-dimensional formula (2π)^{n/2} e^{iπn/4} (det A)^{−1/2} are derived. In the present extended version the free field is completely closed: the Fresnel formula is proved for an arbitrary real symmetric positive-definite action A; a generating functional with an external source is introduced and its value computed; the two-point function ⟨y_p y_q⟩ = i (A⁻¹){pq} is obtained; Wick's theorem is proved, so that the free field is closed not only at the level of the two-point function but at the level of all correlation functions; the oscillating premeasure is embedded into the general theory as a complex cylindrical premeasure and its projective consistency is proved; the value of the HK integral is identified with the Fresnel value; and the passage from the damped Gaussian premeasures to the oscillating one, as the damping is removed, is established. All statements are formalised in Lean 4 on top of Mathlib; no file contains sorry, admit or new axioms, and every principal theorem depends only on propext, Classical.choice and Quot.sound. Six language versions (en, ru, de, fr, ja, zh) are provided.