Existence and Mass Gap of Four-Dimensional Yang-Mills Theory with Lean 4 Formalization

This paper presents a rigorous constructive argument within ZFC set theory addressing the existence and mass gap problem for four-dimensional Yang-Mills theory with compact simple Lie groups, as posed by the Clay Mathematics Institute. Based on a refined variational-spectral framework, the study organizes finite-volume bifurcation constructions, infinite-volume limits, the verification of Osterwalder-Schrader axioms, Hilbert space reconstruction, and spectral analysis into a continuous proof chain. The argument rigorously constructs nontrivial Yang-Mills theory objects on four-dimensional Euclidean space and reduces the mass gap problem to a strictly positive spectral gap for the self-adjoint evolution generator. A parallel Lean 4 formalization architecture is provided to corroborate the main analytical results, facilitating cross-verification of the proof chain and object-level theorems.