Infinite-Dimensional Localization of the Yang-Mills Functional Integral on the Gribov Region: Complex Kuelbs-Steadman Premeasures and a Gauge Bypass of the Singer Barrier

This is the ninth paper of a programme constructing the Feynman functional integral without a Wick rotation, based on the non-absolutely convergent Henstock–Kurzweil (HK) integral and on Kuelbs–Steadman spaces. The subject here is the non-abelian continuum: the configuration space of smooth su(N_c)-valued connections on the four-torus, its cylindrical structure and its complex oscillating Kuelbs–Steadman premeasure; the Yang–Mills action as an HK-integrable functional; the Faddeev–Popov determinant as a Berezin integral; the BRS algebra and the Slavnov–Taylor identities; the first Gribov region; and the localization problem — the CutOut problem — of showing that the contributions from outside the Gribov region cancel in the continuum limit. Every proved statement is proved in full in the main text. The scope is stated honestly. Proved here, in the finite-mode truncation: projective consistency of the non-abelian oscillating cylindrical premeasure; the polynomial structure of the truncated Yang–Mills action and the HK integrability on every compact box; the Berezin representation of the Faddeev–Popov determinant and the explicit linear deformation with positivity radius; nilpotency of the BRS operator, BRS exactness of the gauge-fixing sector and the Slavnov–Taylor identities; openness, non-emptiness, star-shapedness and the boundary description of the first Gribov region; the elementary bound on the cut-out violation functional; and the stability of gauge-invariant averages under refinement of the truncation. The CutOut theorem itself is stated as a paper-level conjecture; what is proved is the conditional statement that the singular-direction hypothesis implies it. The paper does not solve the continuum Gribov problem, and does not attempt non-abelian renormalization, anomalies, or the continuum limit of the abelian CutOut. All the finite-mode statements are machine-verified in Lean 4 with no sorry, no admit and no new axioms; a deterministic numerical script confirms six further checks.