What question did this study set out to answer?

The research aims to establish a proof of the mass gap in Yang-Mills equations on a 4-torus with Klein structure.

January 16, 20260 citationsOpen Access

Yang-Mills Mass Gap via Klein Topology and the Five Pillars

Key Points

The research aims to establish a proof of the mass gap in Yang-Mills equations on a 4-torus with Klein structure.
Utilized Lean 4 for formalizing the proof with no axioms or sorry statements.
Analyzed the properties of Klein4 involution and its impact on determinant.
Examined the behavior of the Levi-Civita tensor under the involution.
Confirmed the existence of a mass gap in Yang-Mills equations on the 4-torus.
Demonstrated that odd integrals over symmetric domains vanish, leading to zero θ-term.
Established that the topological density contributes to ultraviolet regulation.

Abstract

We present a complete machine-verified proof that the Yang-Mills equations on the 4-torus T4 with Klein structure exhibit a mass gap. The proof is formalized in Lean 4 with zero axioms and zero sorry statements for the core theorems. The key insight is that the Klein4 involution has determinant −1, causing the Levi-Civita tensor to flip sign. Since the field strength is even under the involution, the topological density εμνρσFμνFρσ is odd. Odd functions integrate to zero over the symmetric domain, so the θ-term vanishes identically. This provides the UV regulation that generates a mass gap.

问 AI

Bookmark

View Full Paper