Infinite-mode lambda phi^4 as a continuous Henstock-Kurzweil integral in real time: a machine-verified construction

We construct the Feynman functional integral of a quartic scalar field theory in real time, with infinitely many modes and without a Wick rotation, as a Henstock-Kurzweil (HK) gauge integral. In Minkowski signature the quartic interaction contributes the weight exp(-i * lambda * phi^4), a pure phase of unit modulus: it does not improve convergence, and the integral is not absolutely convergent. Starting from the real-time HK machinery of previous works and the finite-mode construction of the non-Gaussian case, which are used as ready proven results, we prove at a fixed Fresnel regulator sigma in (0,1] acting on the free part only: (A) at every mode level M the truncated partition function is an HK integral over every box and for every calibration, with a calibration-independent value, it factorises over the modes, obeys an explicit modulus bound and is of class C^infinity in the coupling and in the source, with explicit bounds on all insertions; moreover, at each fixed mode level the Fresnel boundary limit sigma -> 0+ exists with an explicit linear rate, unconditionally in the free sector and under a displayed one-mode hypothesis for lambda > 0; (B) a uniform one-mode estimate |rho_n - 1| <= 20 * sigma^(-5/2) * (|j_n| * a_n^(-1/2) + lambda * a_n^(-2)) with constants independent of M, and, on the mode lattice Z^d with a_n = |n|^2 + m^2, an explicit tail bound epsilon_M <= 52/M for d <= 3, together with an exponential tail whenever the effective one-mode coupling decays exponentially; (C) existence, uniqueness and calibration independence of the limit M -> infinity, with the rate of (B), and its reduction to the free Fresnel value of previous works at lambda = 0; (D) the exact finite-truncation identity between the zeta-regularised determinant and the free part of the partition function, together with the meromorphic continuation of the lattice spectral zeta function to C with explicit poles, residues and regularity at the origin, and the closed value exp(-zeta_A'(0)) = 4*sinh^2(pi*m) in d = 1; (E) spectrality in the Källen-Lehmann form, real-time (modified reflection) positivity, and microcausality in its equal-time form on the d-dimensional mode lattice; (F) the decision on d = 4: the question is left open (F-open), with a proved obstruction - the mode sum that controls the quartic interaction converges for d <= 3 and diverges for d = 4 - and a conditional positive result in d = 4 with a scale-dependent coupling lambda_M <= C_Lambda * M^(-epsilon), which does not resolve (F-open). All statements are formalised and machine-checked in Lean 4 with Mathlib: no sorry, no admit, no new axioms.