OSTERWALDER–SCHRADER REFLECTION POSITIVITY IN THE COLOUR-SINGLET SECTOR Hᴳ OF T-DFT THE REYNOLDS PROJECTOR AS A KREIN FILTER

Proof of Osterwalder–Schrader Reflection Positivity (OS3) This document proves the Osterwalder–Schrader Reflection Positivity axiom (OS3) for the Yang–Mills theory projected by the Reynolds Projector P̂G. The central difficulty is that Yang–Mills theory with Faddeev–Popov ghosts lives naturally in a Krein space K (a Hilbert space with indefinite inner product), where reflection positivity fails for the full space. Methodology Section 2: HG = P̂GH as the strictly positive part of K Lemma 2. 1 (Gribov copies are non-singlets): Large gauge fluctuations reside entirely in non-trivial adjoint-representation colour sectors; P̂G annihilates them exactly, ensuring the measure dμT-DFT carries no copy contamination. Lemma 2. 4 (BRST filter): Ghost fields carry adjoint colour, so HG ↪ HBRST, which is the positive-definite subspace of K. Section 4: Proving OS3 on HG The proof utilizes: The modular involution JG of Tomita–Takesaki; The reality and positivity of the Euclidean Yang–Mills action restricted to the first Gribov horizon; The annihilation of negative-norm states by the Reynolds Projector. Machine Verification (New in v4) Section 8 presents a Lean 4 formalisation of the algebraic core of the OS3 proof: C₃₁. lean: Closes the theorem OS3ReflectionPositivity with zero sorry occurrences and zero custom axiom declarations. CompanionC3. lean: Encodes the broader OS1–OS5 axiom structure and the reconstruction theorem. Main Result Under the hypotheses of Companions O1–O3 and C2, the projected theory on HG satisfies all five Osterwalder–Schrader axioms. The OS Reconstruction Theorem guarantees the existence of a Wightman QFT with a mass gap M = 8ΛQCD > 0.