Uniformity is the Obstruction: A Machine-Checked No-Go for Uniformly Contracting Multi-Scale Bounds in Lattice Yang–Mills

We report a formally verified negative result concerning a family of strategies for establishing a mass gap in four-dimensional lattice Yang–Mills theory. Working in Lean 4 with a discipline that requires every cited statement to pass both an elaboration check and a kernel axiom audit, we isolate and prove three arithmetic facts. First, the multi-scale curvature-budget criterion of Bauerschmidt–Bodineau, applied to Bałaban block averaging with the Shen–Zhu–Zhu Hessian bound, fails already at the first blocking step: for SU(3) in d=4 the deficit is exactly 132/π² ≈ 13.37, and even the most favourable convention combined with the pre-errata diagonal-only Hessian reduces the closure condition to the false inequality π² ≥ 11. Second, anchoring the criterion at the ultraviolet end is incompatible with the continuum limit: the two requirements jointly admit a single lattice spacing, which we prove is not a limit. Third, we identify the structural property shared by several failed strategies — bound schemes that compose multiplicatively with a per-step factor uniformly bounded away from 1 — and prove that every such scheme collapses under unbounded iteration, while schemes with per-step factor exactly 1 provably lie outside the family. We further observe, by elementary means, that the Osterwalder–Schrader argument establishing H ≥ 0 from reflection positivity is constitutively blind to dimensionful data: its iterated Schwarz step sends any finite constant to 1, annihilating a putative gap as efficiently as it annihilates accumulated debt. A free massive scalar exhibits the same blindness, showing this is a limitation of the proof technique rather than a feature of Yang–Mills. We conclude that the open problem, as it presents itself to constructive methods, is not the existence of the gap but the existence of a bound uniform in the lattice spacing across the strong-to-weak coupling crossover.