The Euclidean Yang–Mills Measure of T-DFT: Existence via the Bochner–Minlos Theorem with Dual Topological Cutoff, and Unconditional Stability via the ERG–DSE–Block-Spin Triple Validation

This document constructs the T-DFT Yang–Mills functional measure dμT-DFT as a σ-additive probability measure on the space of tempered distributions S'(R4) via the Bochner–Minlos theorem. The construction employs a dual topological cutoff: (i) UV cutoff (asymptotic freedom): high-frequency modes k2 ≫ Λ2QCD are suppressed by αs(k2) → 0. (ii) IR cutoff (T-DFT Theorem I 25): the holographic cutoff k2 ≥ Λ2QCD eliminates all massless infrared modes, rendering the Yang–Mills functional integral IR-finite. The document proceeds in three parts. Part I (Sections I–VI) establishes the Bochner–Minlos framework: the lattice regularisation, the characteristic functional ZT-DFTj, and the verification of conditions BM-1 (normalisation) and BM-3 (positive definiteness) unconditionally, together with BM-2 (nuclear continuity) on the lattice. Part II (Sections VII–X) provides the unconditional proof of BM-2 in the continuum limit via the Triple Validation: ERG (Wetterich equation): the T-DFT mass gap M = 8ΛQCD is an exact fixed point of the renormalisation group flow (∂kMT-DFT = 0). DSE (Dyson–Schwinger equations): the projected propagator GG(p2) is uniformly bounded by 1/(2Λ2QCD) for all momenta, with explicit ε-independent constants. Block Spin (Bałaban): the mass gap M(n) = 8ΛQCD is preserved at every level of discrete block integration. Part III (Section XI) synthesises the Triple Validation into the main theorem and its corollaries. Machine verification. The algebraic core of Parts I and II has been formally verified by the Lean 4 proof assistant with the Mathlib library, with zero errors, zero sorry placeholders, and no unsafe axioms. The verified results include the ERG fixed-point identity ∂kMT-DFT = 0, the strict positivity of the Euclidean propagator denominator (Lemma IX.2), and the uniform DSE bound GG(k2) ≤ 1/(2Λ2QCD) (Proposition IX.1). The Lean source code and a complete audit of the six postulates invoked are documented in Supplement A at the end of this document. Main result. The Bochner–Minlos theorem, with all three conditions verified unconditionally, guarantees the existence and uniqueness of dμT-DFT as a σ-additive probability measure on S'(R4), supported on Ω1 ∩ B4/gauge, satisfying the three constraints C1-R1 through C1-R3 identified in Companion C3 (Section 5) as necessary conditions for OS3; C3’s proof of OS3 does not depend on C1 and is logically prior. Combined with the OS Reconstruction Theorem of Companion C3, this establishes the existence of a Wightman Yang–Mills QFT on Minkowski space with a strictly positive mass gap Δ = 8ΛQCD > 0. The global implications of this result for the complete T-DFT programme are documented in the Master Synopsis 27.