Construction of Kuelbs–Steadman Spaces and Gauge Closure of the Feynman Functional Integral in Lean 4

This report completes the three missing ingredients of the infinite-dimensional Henstock–Kurzweil (HK) programme, and machine-checks all of them in Lean 4 with Mathlib. First, the Kuelbs–Steadman space KS₂ is constructed concretely as the separable real Hilbert space H carried by the weighted inner product attached to an orthonormal total family of modes and a strictly positive summable weight sequence; the inclusion H ↪ KS₂ is shown to be a continuous linear map, the coordinate functionals to be KS₂-continuous, and the image of every ball of H to be totally bounded in KS₂, hence relatively compact in its completion. The proof proceeds through a uniform tail estimate which is exactly the input required by the Gill–Kuelbs argument. Second, KS₂ is registered as an instance of the abstract cylindrical gauge space of the previous stage, and the general cylindrical Cousin lemma with varying direction spaces is obtained from it via the global K₀-reduction. Third, the splitting lemma is proved: coordinate hyperplanes are null for the finite-dimensional Gaussian measure, and every δ-fine division of a cylinder over a box into cylinders over boxes can be refined, with unchanged Riemann sum and without losing δ-fineness, into one whose cells lie entirely on one side of a coordinate hyperplane. Finally the finite-dimensional consistency theorem is established. Every statement listed in Section 5 compiles in Lean 4 without sorry, without admit, and depends only on the three standard axioms propext, Classical.choice, Quot.sound.