A Geometric and Metric-Measure Framework for the Yang–Mills Mass Gap

This paper studies the Gribov–Zwanziger formulation of Yang–Mills theory as a metric-measure problem and separates what is proved from what is assumed. It does not solve the Yang–Mills existence and mass gap problem. The mass-gap result is conditional only: it holds if (i) regularized ground-state measures on the Gribov region satisfy a uniform Bakry–Émery curvature bound CD(K,∞), and (ii) the corresponding Hamiltonians converge in the strong resolvent sense after an isometric identification of their Hilbert spaces. Under those two unproved hypotheses, the continuum Hamiltonian has a gap of at least g²K/2. Neither hypothesis is established here; no mass gap is claimed. Proved unconditionally: on every finite-dimensional Galerkin truncation of the Gribov region, in flat Landau-slice coordinates, the Faddeev–Popov log-determinant and the horizon function are convex, with an analogous statement for lattice SU(2) in one gauge chart. The strong-convexity modulus of the horizon function tends to zero as the truncation cutoff is removed, so this convexity gives no uniform curvature bound and does not establish hypothesis (i). Several smaller facts (linearity of the gap criterion in K, exact L^(1/2) scaling of the distance to the Gribov horizon, infinite Federer reach of the closure of the convex Gribov region, a tree-level estimate) are proved with stated scope. Known Bakry–Émery bounds for strongly coupled lattice Yang–Mills theory are discussed; they do not supply hypothesis (i). Formal verification. Selected elementary statements of this paper are formalized in Lean 4 with Mathlib (no `sorry`, no added axiom; `#print axioms` reports only the standard axioms) in the folder `formal_proofs_mathlib` of the author's repository, modules `LeanReal/YangMills`, `YangMills_Y4`, `YangMills_Y4a` and `YangMills_Y5`, each as a declared reduction stated in that folder's README: YangMills — the convexity of the Gribov region and that 0 lies in it, for an abstract affine pencil in any real vector space, with M₀ > 0 as a hypothesis (Prop. 4.2(a)); the unique nearest point in its closure, in a complete real inner-product space (Prop. 4.2(d); Federer's reach itself is not formalized); the tree-level bound k² + λ⁴/k² ≥ 2λ² with its equality case, algebraically (the Gribov–Zwanziger quadratic form is not derived); YangMills_Y4 — the convexity and strict convexity of −log det on the positive-definite cone and on Galerkin pencils, strict iff the pencil map is injective (Lemma 4.6(b); part (a) and the boundary limit are not in this module); YangMills_Y4a — the symmetry and affinity of M_N and that the truncated region is open, convex and contains 0 (Lemma 4.6(a)), in an abstract integration-by-parts model where two torus facts are hypotheses and the model is proved only for the circle T¹ (the Faddeev–Popov operator is not formalized); YangMills_Y5 — the range of the tight-binding band E(θ) = −2t cos θ and the finite circulant ring (Prop. on tight binding; the spectrum on ℓ²(ℤ) is not proved). Negative controls (`mutant_gribov_nonaffine`, `mutant_tree_level`) are proved false in the same modules. The paper's own Verification-status paragraph now names all four modules by name, including Lemma 4.6(a) (`YangMills_Y4a`). The mass gap, the conditional theorem, its hypotheses, items (b)–(c) of Prop. 4.2 and reach(Ω) = 0 are not formalized. The older Lean 4 files in `formal_proofs_yang_mills` are a placeholder skeleton without Mathlib and verify none of the mathematics. Repository: https://github.com/reinaldomsilvafilho-netizen/quantum-gravity-lean4 Use of AI and status. Large language model assistants (Anthropic Claude; Google Gemini) were used extensively, as disclosed in the paper's Declarations, in line with the Leiden Declaration on Artificial Intelligence and Mathematics (arXiv:2609.35334): the mathematics was checked by AI sessions that had not written it (blind review, independent correction, targeted re-check). These checks are not peer review. This is a preprint: Zenodo is a repository, not a peer-reviewed venue, and no result has yet been checked by an independent human expert. Funding: CAPES, Finance Code 001.