The First Gribov Region, BRS Symmetry and Slavnov-Taylor Identities in the Truncated Henstock-Kurzweil Yang-Mills Theory

Abstract

This is the seventh paper of the programme devoted to the construction of the Feynman functional integral without Wick rotation, based on the non-absolutely convergent Henstock–Kurzweil (HK) integral and on Kuelbs–Steadman spaces. In the truncated Yang–Mills theory on TL3×Sβ1TL3×Sβ1, constructed in the previous two papers, we build and machine-verify four structures: (A) the first Gribov region ΩN,KΩN,K, of which we prove openness, non-emptiness and star-shape with respect to the origin, together with the description of its boundary as the locus of a non-constant zero mode of the Faddeev–Popov operator; (B) the BRS transformation ss on the truncated configuration space with ghosts, its nilpotency s2=0s2=0 on all fields and on the whole algebra they generate; (C) the BRS invariance of the full action SYM+Sgf+SghSYM+Sgf+Sgh, obtained from the BRS exactness of the gauge-fixing sector, and the Slavnov–Taylor identities in the truncated theory, in an analytic form and in an algebraic form; (D) the stability of normalised gauge-invariant averages under the truncation parameters (N,K,L)(N,K,L). The HK integral restricted to ΩΩ is shown to exist on every compact box for every gauge integration filter. Parts (A)–(D) are theorems of the truncated, finite-dimensional theory and are formalised in Lean 4 without sorry and without new axioms; the continuum double limit (N,K,L)→∞(N,K,L)→∞ with the automatic cut-out of ΩΩ is formulated as a conjecture and is not proved. A deterministic numerical script confirms all six checks, including the honest negative one: in the truncated theory the contributions from B∖ΩB∖Ω do not cancel.