Vacuum-sector mass gap for the local gauge-invariant sharp-local Yang–Mills net

Description This work presents a theorem establishing a vacuum-sector mass gap for the bounded-region local gauge-invariant sharp-local Yang–Mills net associated to any compact connected simple gauge group GGG. The proof is organized through a finite packet reduction architecture consisting of: a compact-simple ultraviolet gate, a Route 1 lattice-to-continuum vacuum-gap chain, a Lane A sharp-local constructive chain, and a theorem-level endpoint packet (OS/Wightman reconstruction and local-net identification). The theorem-level object is explicitly local: the result applies to the bounded-region gauge-invariant sharp-local net generated by flowed curvature composites. Extended-support line and surface sectors are excluded from the theorem claim. Formal Verification Layer The manuscript is accompanied by a Lean4 formal verification layer that certifies the theorem-level dependency structure and closure architecture. The Lean development verifies: packet routing and reduction, dependency DAG and theorem ownership, closure interfaces across Route 1, Lane A, and endpoint assembly, non-circularity of the proof spine, consistency between manuscript claims and proof structure. The Lean layer operates relative to an explicitly declared imported substrate: standard Wilson lattice Yang–Mills theory, standard Osterwalder–Schrader reconstruction framework. Formalization of this standard substrate is outside the scope of the present verification layer. Main Result (informal summary) The constructed sharp-local Yang–Mills theory satisfies: existence of a continuum local gauge-invariant quantum field theory, OS/Wightman reconstruction, Haag–Kastler local net structure, non-triviality (nonzero spectral weight), and a strictly positive vacuum mass gap: Spec(H)⊂{0}∪[m∗,∞),m∗>0.\mathrm{Spec}(H) \subset \{0\} \cup [m^*, \infty), \quad m^* > 0.Spec(H)⊂{0}∪[m∗,∞),m∗>0. The continuum local theory is faithful-Wilson universal at theorem level: all faithful ultraviolet Wilson regularizations of the same group GGG yield canonically isomorphic local theories (qualitatively). Explicit quantitative bounds remain indexed by the chosen ultraviolet regularization. Scope Clarifications This work does not claim: a mass gap for nonlocal sectors (line/surface operators), uniform quantitative bounds across all faithful representations, formalization of the Wilson QFT substrate in Lean, results outside the admissible gradient-flow renormalization class. Structure of the Archive The Zenodo record includes: Core manuscript (theorem and proof spine) Companion I: ultraviolet gate and Route 1 chain Companion II: Lane A constructive chain Companion III: reconstruction and endpoint packet Lean4 verification layer (dependency and closure certification) Significance The contribution is twofold: A constructive Yang–Mills mass-gap proof framed at the level of local nets. A machine-verified proof architecture that eliminates hidden dependencies and enforces explicit theorem-level closure.