Yang–Mills as a Henstock–Kurzweil integral without gauge fixing: a structural bypass of the Gribov ambiguity

In the Henstock–Kurzweil (HK) programme for the real-time functional integral, the previous works attacked the Gribov problem from inside the standard Faddeev–Popov scheme, and earlier it was honestly reported that the fixed-epsilon CutOut question is open, with three attack routes closed. The present work does not continue that attack. It changes the question: instead of asking how to handle Gribov copies, it asks why they are created at all. We define the Yang–Mills functional integral on the finite-mode truncation A_N of Yang–Mills on T^4 without fixing the gauge: no delta function of a gauge condition, no Faddeev–Popov determinant, and no choice of representative on an orbit enters the definition. Physical quantities are defined as ratios of two such integrals of gauge-invariant functionals, in which the (formally infinite) orbit volume cancels. We prove, at finite mode truncation and with every constant explicit: (A) the unfixed HK integral exists, is independent of the calibration and equals the Lebesgue integral of the same integrand; (B) the denominator is non-zero, with the explicit lower bound cos(beta(R)) (2R)dim A_N, for boxes B_R containing the origin, whenever the explicit action bound beta(R) = q_2 R^2 + q_3 R^3 + q_4 R^4 is smaller than pi/2 (for a box not containing the origin the denominator may vanish, and an explicit example is given); (C) two Gribov copies of a configuration contribute identical terms to every Riemann sum of the unfixed integral, so that no choice between them is ever required; the definition itself does not use the gauge-fixing data, whereas — by contrast — the gauge-fixed construction genuinely depends on the prescription; (D) the normalised averages are consistent under mode truncation: they are equal when the action decouples, differ by at most C epsilon in general, and converge, with an explicit rate, under an explicit hypothesis (T) on the coupling between retained and boundary modes, the limit being independent of the chosen sequence of truncations; (T) is shown to be neither vacuous nor automatic; (E) at weak coupling the unfixed average reproduces the Faddeev–Popov average to order g^2, with an explicit constant, under the quantitative perturbative hypothesis (H) on the Faddeev–Popov weight; (H) is itself derived, with an explicit constant, from the affine dependence of the lattice Faddeev–Popov matrix on the configuration. All five theorems, and the propositions accompanying (T) and (H), are proved in full in the main text; the machine-verified part is formalised in Lean 4 / Mathlib without sorry, without admit and without new axioms, and the precise boundary between what is and what is not formalised is stated in the dedicated section. A deterministic script illustrates the statements numerically. We explicitly do not claim that the Gribov problem is solved, nor a continuum limit, nor renormalisability, nor a mass gap. We distinguish two levels of bypass: Level One, realised here, in which the gauge is never fixed, and Level Two, in which gauge orbits would not exist at all (the loop representation), which is stated as future work and is used in no theorem.