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

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. The T-DFT argument resolves this in two steps. Section 2: We prove that HG = P̂GH is the strictly positive part of the Krein space K. The key ingredient is that Faddeev–Popov ghost fields carry colour in the adjoint representation and are therefore not colour singlets — P̂G annihilates them exactly. Formally: HG ↪ HBRST (BRST cohomology), which is known to be the positive-definite subspace of K (Lemma 2. 2). Section 4: We prove OS3 on HG using: (a) the modular involution JG of Tomita–Takesaki established in Companion C2 17; (b) the reality and positivity of the Euclidean Yang–Mills action restricted to the first Gribov horizon (IR cutoff of Theorem I) ; (c) the annihilation of negative-norm states by the Reynolds Projector. The complete OS axioms OS1–OS5 are verified in Section 5. By the Osterwalder–Schrader Reconstruction Theorem (Section 6), the T-DFT Yang–Mills theory in the sector HG admits a Wightman QFT on Minkowski space. Section 7 records the fulfillment of all three constraints (C1-R1 through C1-R3) by the Triple Validation construction of Companion C1 16 (ERG + DSE + Block Spin). Machine verification (new in v4). Section 8 presents a Lean 4 14 formalisation of the algebraic core of the OS3 proof. The primary file C₃₁. lean (namespace TDFTC3) closes the theorem OS3ReflectionPositivity with zero sorry occurrences and zero custom axiom declarations, using only the standard Mathlib4 15 library. A secondary file CompanionC3. lean (namespace TDFT) encodes the broader OS1–OS5 axiom structure and the reconstruction theorem in a complementary formalism. Main result. Under the hypotheses of Companions O1–O3 and C2, the projected theory on HG satisfies all five Osterwalder–Schrader axioms, and the OS Reconstruction Theorem guarantees the existence of a Wightman QFT with a mass gap M = 8ΛQCD > 0.