Infinite-dimensional Henstock–Kurzweil integral: Rigorous Construction of the Feynman Functional Integral in Lean 4

This report continues a programme aimed at a fully formalised theory of the Henstock–Kurzweil (HK) integral on infinite-dimensional separable Hilbert spaces, the natural setting for the functional integral ∫ F(φ) D_HK φ. The first two steps — cylindrical sets and the algebra they form, and gauges, tagged partitions and δ-fineness — are briefly recalled. Three new steps are carried out and machine-checked in Lean 4. First, cylindrical premeasures are defined, together with projective consistency in the form of the Kolmogorov identity; consistency is proved transitive along chains, invariant under pointwise equality of the underlying family, and satisfied by the zero family and by Dirac masses at the origin. Second, the finite-dimensional Cousin lemma is recorded in the exact half-open and open-box forms needed below. Third, the cylindrical Cousin lemma for a fixed direction space is proved: over a finite-dimensional V = span(e_1,...,e_k), and for a gauge constant on the fibres of the projection onto V, every cylinder over a box admits a δ-fine tagged family of cylinders over the same V, pairwise disjoint and with union exactly the given cylinder. The standard Gaussian cylindrical premeasure on a separable Hilbert space with a fixed orthonormal basis is then constructed and proved projectively consistent: for finite-dimensional V ≤ W and arbitrary base B, one has μ_W(pr_V^{-1}(B) ∩ W) = μ_V(B). The proof splits W orthogonally as V ⊕⊥ (W ∩ V⊥), factorises the Gaussian density along the splitting, and cancels the normalisation constant of the complementary factor against its Gaussian integral. This is the first non-trivial projectively consistent family in the development. Two further steps are carried out. Abstract cylindrical gauge spaces are introduced, axiomatising the properties expected of a Kuelbs–Steadman space: a countable orthonormal family of modes, an auxiliary topology with continuous coordinates, and compactness of finite-dimensional blocks. The global K0-reduction is proved: for a coordinate-sequential gauge constant on the fibres of pr_{V_n}, the number of modes required on a cylinder over a box is uniformly bounded, and the Cousin problem for that cylinder is solved by the fixed-direction-space lemma over the single subspace V_n. Finally, the HK functional integral with respect to a cylindrical premeasure is defined as the limit of Riemann sums along the filter of δ-fine divisions, and uniqueness, linearity, additivity over disjoint cylinders, finite additivity of a projectively consistent premeasure along a division with cells over different direction spaces, and exactness of the integral of a constant are proved. For the Gaussian family this gives the finite-dimensional Gaussian measure of the base. All Lean files compile against current Mathlib without sorry, admit, or any new axiom. The paper also adds two paper-level layers. First, the three criteria previously described discursively — projective localisability (uniform tail decay), strong-operator analyticity of the nonlinear generator, and alternating-sign phase interference — are turned into the hypotheses of a single general gauge-compatibility theorem, which concludes HK-integrability of a non-Gaussian functional F = exp(-S_int) on the whole space, uniqueness of the Riemann-sum limit, and convergence of the Chernoff time-splitting (e^{tA_0/N} e^{tB_λ/N})^N; the link between the first two criteria is made explicit, and the non-stationary-phase estimate |∫_{C_j} e^{iS} dμ| ≤ C ε(t_j)/||∇S(t_j)|| behind the third one is stated and used. Second, a section of applied consequences shows how the machinery recovers the classical first anharmonic correction ∂_λ⟨x^2⟩|_0 = -12T^3 for the Duffing oscillator directly as a convergent HK expression, and yields a non-perturbative formula for the first-order volatility-smile shift in CEV local-volatility models, ∂_λ log F_λ(j)|_0 = -Σ_i M_4(ω_i,j_i,0)/M_0(ω_i,j_i,0), with remainder controlled by λ M_8 and no Monte-Carlo simulation. The gauge-compatibility theorem and the financial formula are stated at paper level and, like the other unformalised material, are kept strictly out of the Lean files; the Duffing constant, by contrast, is machine-checked in a new Lean file, which computes the Gaussian moments M_0, M_2, M_4, M_6 from the integration-by-parts recursion and proves (M_6 M_0 - M_2 M_4)/M_0^2 = 12T^3.