The Yang–Mills Functional Integral on Finitely Many Fourier Modes on the Torus T⁴ as a Henstock–Kurzweil Path Integral: Gauge Fixing, the Ghost Sector, and Gribov Copies

Abstract

This is the fifth paper of the programme constructing the Henstock–Kurzweil (HK) functional integral without Wick rotation, and the first in which the bosonic sector, the ghost sector and the oscillating premeasure are combined in a single formula. The price of this combination is a truncation: Yang–Mills theory is considered on finitely many Fourier modes on the four-torus T⁴. We define the truncated configuration space V_N of dimension 32(2N+1)⁴, the truncated Yang–Mills action as a real polynomial of degree four on V_N, the truncated gauge group G_N (in the linear realisation preserving V_N), and the truncated Faddeev–Popov operator together with its Berezin representation. The combined integrand I_N(F,A) = F(A)·Δ_FP^(N)(A)·exp(i·S_YM^(N)(A)) is Henstock–Kurzweil integrable on every compact box B ⊂ V_N; the HK integral is linear in the observable and additive in the box. We then study the Gribov copies of the truncated theory: copies exist (explicitly — in a one-dimensional toy model of an orbit, and numerically for SU(3)), the Faddeev–Popov determinant depends on the copy, and the normalised averages of gauge-invariant observables do not. All of these statements, in their formalised finite-dimensional form, are machine-verified in Lean 4 (Mathlib) and contain no sorry and no new axioms. What the paper does not do is stated explicitly: the continuum Yang–Mills functional integral is not constructed, only its spectral truncation is; the limit N → ∞ for the combined integrand is left as future work. Two language versions (English and Russian), the Lean 4 formalisation, and the numerical verification script are provided.