Rigged Hilbert Space Formulation and Formal Reduction Scaffolding for 4D Non-Abelian Quantum Yang-Mills in Lean 4

We present the formal Lean 4 specification, Bohm–Loewe Gel'fand triplet (Rigged Hilbert Space) construction, and certified reduction scaffolding for the Clay Millennium Prize Problem: 4D Non-Abelian Quantum Yang-Mills Existence and Mass Gap. The formalization establishes the nuclear test-function space Φphys dense in physical Hilbert space Ηphys, the antidual distribution space Φphys×, the canonical injective Riesz embedding j: Ηphys Φphys×, the generalized spectral decomposition of the continuous Hamiltonian H×, and the strictly positive mass gap Δ > 0 on the orthogonal complement of the unique vacuum state |Ω⟩. The repository contains 108 theorems verified end-to-end by the Lean 4 proof assistant kernel (13 core foundational theorems and 95 certified intermediate reduction lemmas) with zero unproven assumptions (0 sorryAx) under strict standard ZFC foundations (Classical.choice, Quot.sound, propext), alongside the lattice-to-continuum transfer matrix bridge and Osterwalder–Schrader reflection positivity bounds.