The Faddeev–Popov Determinant and the Henstock–Kurzweil Path Integral: Berezin Representation, Spectral Limit, and Gribov Copies

Abstract

This is the fourth paper of the programme constructing the Feynman path integral as a Henstock–Kurzweil (HK) integral without a Wick rotation, and the first one dealing with the gauge (ghost) sector of a non-abelian theory. The Faddeev–Popov determinant is constructed as an algebraic object and identified with a Berezin integral over ghosts: for every complex N×N matrix M the identity ∫ Dc Dc̄ exp(c̄ M c) = det M is proved (Theorem 4.1), whence the Berezin representation of the lattice Faddeev–Popov determinant on the 2⁴ lattice, with a 128×128 matrix (Theorem 4.2). Both statements are fully formalised in Lean 4 (Mathlib) and contain no sorry and no new axioms. Spectral truncation on the four-torus T⁴ is then introduced: Laplace eigenfunctions, projectors P_N, truncated matrices M_FP^(N) and truncated determinants; their Berezin representation is machine-verified as well (Theorem 5.4). The limit N → ∞, which produces the ζ-regularised determinant of the continuum Faddeev–Popov operator, rests on the classical ζ-regularisation theory of elliptic operators and is not machine-verified in the present work; what is proved in Lean is the uniqueness of such a limit. Finally, two statements about Gribov copies are carefully separated: the Faddeev–Popov determinant does depend on the copy (Theorem 7.1, machine-verified in the SU(2) one-link model and checked numerically for the SU(3) lattice), whereas the normalised average of a gauge-invariant functional F does not (Theorem 7.2, whose finite-dimensional core is formalised). The numerical program verify_fp.py reproduces all the checks. The full bosonic Yang–Mills HK integral is not constructed in this paper. Two language versions (English and Russian) are provided; the Lean 4 formalisation and the numerical verification script are included.