Show HN: Zero-axiom Lean 4 proof that Yang-Mills on R^4 is a "round square"

The Lean 4 file presents a claimed negative resolution of the Yang-Mills mass-gap problem on pure, non-compact ℝ⁴. Its central claim is that the Osterwalder-Schrader/Wightman conditions and a strict spectral mass gap are mutually incompatible within a “canonical” class of theories: satisfying the first rules out the gap, while enforcing the gap rules out the first. The file distinguishes this universal exclusion from two proposed witness cases - one with the axioms but no gap, another with a gap but not the axioms - and supplies general logical definitions for what it calls a complete negative-result resolution. It also advertises a formal audit with no `sorry`, custom axioms, or specified classical-choice dependencies.

The key issue is that formal verification establishes only the Lean propositions as encoded; it does not by itself show that those propositions accurately capture Yang-Mills theory or that the claimed incompatibility follows from established analysis. In the excerpt, the general exclusion result follows directly from a stipulated mutual-exclusion condition, while the physical meanings of the theory class and its requirements depend on the later formal definitions and proofs. Thus, the file’s significance rests on whether its formal model faithfully represents the analytic and physical problem - not merely on whether Lean accepts the code without extra axioms. It is best understood as a formalized claim and proposed framework, rather than an independently demonstrated resolution of the Clay problem.