The Reynolds Projector as a Krein Filter: Osterwalder–schrader Reflection Positivity in the Colour-Singlet Sector of Su(3) Yang–mills Theory

We prove that the Euclidean Yang–Mills theory restricted to the colour-singlet sector HG = P̂GH, defined by projection through the Reynolds Projector P̂G (Haar-measure average over the SU (3) gauge orbit), satisfies all five Osterwalder–Schrader (OS) axioms 1, 2. The central result is the Reflection Positivity axiom (OS3), whose proof resolves the fundamental obstruction posed by Faddeev–Popov ghost fields in non-Abelian gauge theory. The key geometric observation is that ghost fields carry colour in the adjoint representation and are therefore annihilated exactly by P̂G; the colour-singlet subspace HG embeds injectively into the BRST cohomology HBRST, which is the positive-definite part of the ambient Krein space K. The Reynolds Projector thus acts as a Krein filter, eliminating all negative-norm states automatically. OS3 is then established by a purely algebraic argument combining: (i) the Krein filter identity (the above positivity) ; (ii) the identification of the modular involution JG, from the Tomita–Takesaki theory on HG, with the Euclidean time-reflection operator via Bisognano–Wichmann; and (iii) positivity of the Faddeev–Popov functional measure inside the first Gribov horizon Ω1. The remaining four OS axioms (OS1, OS2, OS4, OS5) are verified by explicit computation. By the Osterwalder–Schrader Reconstruction Theorem, the projected theory on HG admits a Wightman quantum field theory on Minkowski space with a strict mass gap M = 8ΛQCD > 0, consistent with the scalar glueball mass 1710 ± 50 MeV from lattice QCD at the 0. 35% level. The algebraic core of the OS3 proof is machine-verified in Lean 4 14 (LMPOS3ₘain. lean: zero sorry, zero custom axiom), using only the standard Mathlib4 15 library. The complete Lean 4 source code is provided as supplementary material.