The Wilson-loop formulation of Yang–Mills at finite mode truncation: a Level-Two structural bypass of the Gribov ambiguity

The unfixed real-time Henstock–Kurzweil (HK) functional integral for truncated Yang–Mills removes the choice of a gauge surface, but gauge orbits remain objects of the formulation: that is a Level-One bypass of the Gribov ambiguity. The present paper carries out a Level-Two bypass at finite mode truncation: the Wilson loops W(C) are taken as the fundamental variables, so that the configuration space of the theory is a space of loop data and no gauge field, gauge orbit, gauge-fixing condition or Faddeev–Popov determinant occurs anywhere in the formulation. Nine statements are proved, and all of them are machine checked in Lean 4 without sorry, without admit and without new axioms:(A) the loop algebra of Wilson loops of based closed lattice words is a commutative C-algebra, closed under complex conjugation, whose elements are gauge-invariant functionals, with loop variables bounded by one and with the Mandelstam identity tr(AB) + tr(AB⁻¹) = tr A · tr B holding for SU(2);(B) the truncated Yang–Mills action is the evaluation of an explicit multivariate polynomial of total degree at most one in the plaquette Wilson variables, hence a cylindrical function on loop space supported on the loops of length four;(C) every loop-expressible gauge-invariant functional is a cylindrical function of finitely many Wilson loops;(D) the Wilson-loop integrand Φ(W) exp(iS(W)) is HK-integrable on every bounded box of the loop space for every integration calibration, with value the Lebesgue value;(E) the Level-Two integral is a constant function of the gauge-fixing data, and configurations on one gauge orbit — in particular Gribov copies — are the same point of the loop formulation, so the Gribov ambiguity is structurally absent rather than cancelled;(F) for loop observables the Level-Two integral taken with respect to the push-forward of the Level-One measure coincides with the Level-One unfixed HK integral;(G) the one-plaquette SU(2) check is proved in full, including the closed form (2/π)∫₀^π eiβ cos θ sin²θ dθ = 2J₁(β)/β, obtained analytically by term-by-term integration, with J₁ defined by its everywhere convergent power series.Two further results extend the v1 formulation: (C′) the Mandelstam relations for SU(N), derived in manifestly covariant trace form from the vanishing of the antisymmetriser AN+1 on (C^N)⊗(N+1) together with the rank-N Cayley–Hamilton theorem, and written out explicitly for SU(3); and (H) projective compatibility across mode levels: for a cylindrical loop functional of bounded mode support the finite-M Level-Two integrals coincide, so that they form a projective system whose limit exists as a linear functional — not a measure — on the union of the loop algebras.No continuum limit, no mass gap, no confinement and no Makeenko–Migdal equation is claimed; the Giles reconstruction theorem is used only as a cited black box, and no stack- or sheaf-theoretic refinement of it is attempted. The honest report in §13 records exactly where each proof stops. The paper is accompanied by a complete Lean 4 / Mathlib formalisation (nine files, 138 audited declarations, no sorry, no admit, no new axioms) and by a deterministic Python script that regenerates all numerical checks and all six figures.