Zero-axiom Lean 4 formal proof (RoundSquare.lean, 74 print axioms checks) of the Yang–Mills Mass Gap Incompatibility Theorem on pure non-compact R^4 & automatic spectral gap on the compact constructible manifold M_tot = S^4 x T^3. Official repository for V. Logvinovich (2026)
