Yang–Mills existence and mass gap on $\mathbb{R}^4$ for any compact simple gauge group (Clay Millennium Prize Problem, lattice formulation of Jaffe–Witten §6.5)

Open

YangMills.existence_and_mass_gap

by korbonits · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

constructive-qftgauge-theorylattice-gauge-theorymass-gapmathematical-physicsmillennium-prizeyang-mills

This is the Clay Millennium Prize Problem of Jaffe and Witten (p. 6): "Prove that for any compact simple gauge group $G$ , a non-trivial quantum Yang–Mills theory exists on $\mathbb{R}^4$ and has a mass gap $\Delta > 0$ . Existence includes establishing axiomatic properties at least as strong as those cited in [Streater–Wightman, Osterwalder–Schrader]", stated in the form Jaffe–Witten describe in §6.5: as the existence of the continuum and infinite-volume limit of Wilson's lattice gauge theory with the properties of a reflection-positive Euclidean theory with a mass gap.

Let $G$ be a compact Hausdorff group which is a compact simple gauge group (connected, non-abelian, every closed normal subgroup finite or all of $G$ ), and let $\rho : G \to U(N)$ be a continuous injective homomorphism (so $G$ is a compact Lie group with simple Lie algebra). Then there exist

inverse couplings $\beta_k > 0$ and physical box sizes $L_k \to \infty$ indexed by the lattice spacing $2^{-k}$ ,
positive renormalization constants $Z_k(\gamma)$ for every dyadic loop $\gamma$ in $\mathbb{R}^4$ ,
a functional $W$ on finite families of dyadic loops in $\mathbb{R}^4$ ,

such that:

(Existence of the theory) for every admissible family $A$ of loops (simple, pairwise disjoint),

\prod_{\gamma \in A} Z_k(\gamma)\cdot\Big\langle \prod_{\gamma\in A}\operatorname{tr}\rho(U_\gamma)\Big\rangle_{k,\,L_k,\,\beta_k} \longrightarrow W(A) \qquad (k\to\infty),

where $\langle\cdot\rangle_{k,L,\beta}$ is the Wilson lattice gauge theory expectation at lattice spacing $2^{-k}$ in the box of physical half-side $L$ with action $\beta\sum_p \operatorname{Re}\operatorname{tr}\rho(U_p)$ and free boundary conditions; 2. (Euclidean invariance, lattice part) $W$ is invariant under all dyadic translations and all signed coordinate permutations of $\mathbb{R}^4$ ; 3. (Reflection positivity) for all $c_i\in\mathbb{C}$ and admissible families $A_i$ of loops with strictly positive time coordinates, $\sum_{i,j}\overline{c_i}c_j\,W(\theta A_i\cup A_j)$ is real and $\ge 0$ , $\theta$ the time reflection (with orientation reversal); 4. (Mass gap) there is $\Delta > 0$ such that for all admissible $A, B$ there is $C$ with $|W(A\cup\tau_t B) - W(A)W(B)| \le C e^{-\Delta t}$ for all dyadic times $t \ge 0$ at which $A\cup\tau_tB$ is admissible, $\tau_t$ the forward time translation; 5. (Non-triviality: $m<\infty$ ) property 4 does not hold for every $\Delta$ , i.e. the mass $m = \sup\{\Delta\}$ is finite.

Under Osterwalder–Schrader reconstruction, property 3 yields the Hilbert space, vacuum and positive Hamiltonian $H$ of the theory, and property 4 is equivalent to $H$ having no spectrum in $(0,\Delta)$ ; property 5 is Jaffe–Witten's requirement "we require $m < \infty$ " and excludes the degenerate limits (independent links, flat connections, bounded couplings) whose connected correlations vanish at all large time separations. This is an open problem; a proof would settle the Millennium Prize Problem in this formulation.

Formalization Note The theory is defined through Wilson-loop correlation functions of axis-parallel loops with dyadic vertices (YangMills.Loop 4), following Jaffe–Witten §6.5, Seiler and Chatterjee; smeared field operators and full Euclidean invariance are not encoded. The infinite-volume limit is taken jointly with the continuum limit along $L_k \to \infty$ (weaker than requiring the infinite-volume limit at each fixed spacing). The renormalization constants are multiplicative and per loop, as expected from the perimeter divergence of Wilson loops; they cannot create time dependence in connected correlations. Nothing is asserted about the values of $W$ on non-admissible families, about uniqueness of the theory, about the rate at which $\beta_k \to \infty$ , or about matter fields.

Preamble

import Definitions.Def_YangMills
import Mathlib

Formal statement

namespace YangMills
theorem existence_and_mass_gap {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [MeasurableSpace G] [BorelSpace G]
    (hG : IsCompactSimpleGaugeGroup G) {N : ℕ} (ρ : G →* Matrix.unitaryGroup (Fin N) ℂ)
    (hρ : Continuous ρ) (hρ' : Function.Injective ρ) :
    ∃ (β : ℕ → ℝ) (L : ℕ → ℕ) (Z : ℕ → Loop 4 → ℝ) (W : List (Loop 4) → ℂ),
      IsContinuumLimit ρ β L Z W ∧ IsLatticeInvariant W ∧ IsReflectionPositive W ∧
      (∃ Δ : ℝ, 0 < Δ ∧ HasMassGap W Δ) ∧ HasFiniteMass W := by sorry
end YangMills

Source

A. Jaffe, E. Witten, Quantum Yang–Mills theory, Clay Mathematics Institute Millennium Prize Problem description (2000), https://www.claymath.org/wp-content/uploads/2022/06/yangmills.pdf, p. 6, §4, boxed statement 'Yang–Mills Existence and Mass Gap' and the preceding definition of the mass gap; p. 11, §6.5 for the lattice formulation ('limits of appropriate expectations of gauge-invariant observables as the lattice spacing tends to zero and as the volume tends to infinity'); p. 12, footnote 2 (weak existence excluded unless the properties of the limit are established). Probabilistic formulation: S. Chatterjee, Yang–Mills for probabilists (2019), Problems 5.1 and 5.2, https://doi.org/10.1007/978-3-030-15338-0_1; E. Seiler, Gauge Theories as a Problem of Constructive QFT and Statistical Mechanics, LNP 159 (1982), Ch. 8

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Read-back: `YangMills.existence_and_mass_gap`

1. Hypotheses (everything that is assumed)

The statement is universally quantified over the following data.

A type $G$ carrying: a group structure; a topology; the assumption that the topology makes $G$ a topological group (multiplication and inversion continuous); the assumption that $G$ is a compact space; the assumption that $G$ is Hausdorff ( $T_2$ ); a $\sigma$ -algebra on $G$ ; and the assumption that this $\sigma$ -algebra is the Borel $\sigma$ -algebra of the topology.
A proof $h_G$ $h_{G}$ that $G$ $G$ is a "compact simple gauge group" in the following custom sense (this is a conjunction of three conditions and nothing else; compactness is not part of it, it comes from the separate typeclass assumption above):
1. $G$ is a connected topological space (in particular non-empty);
2. $G$ is non-abelian: $\exists\, a, b \in G$ with $ab \neq ba$ ;
3. for every subgroup $K \le G$ that is normal and whose underlying set is closed in $G$ : either the underlying set of $K$ is finite, or $K = G$ .
A natural number $N \in \mathbb{N}$ (implicit; it may be $0$ ).
A group homomorphism $\rho : G \to \mathrm{U}(N)$ , where $\mathrm{U}(N)$ is Mathlib's Matrix.unitaryGroup (Fin N) ℂ: the set of $N\times N$ complex matrices $U$ with $U^{*}U = 1$ and $UU^{*} = 1$ ( $U^{*}$ = conjugate transpose), a group under matrix multiplication.
A proof $h_\rho$ that $\rho$ is continuous, where $\mathrm{U}(N)$ carries the subspace topology from $\mathbb{C}^{N\times N}$ (product topology).
A proof $h_{\rho}'$ that $\rho$ is injective.

Degenerate values of $N$ . For $N = 0$ the group $\mathrm{U}(0)$ has exactly one element, and for $N = 1$ it is the abelian group $\mathrm{U}(1)$ . In either case injectivity of $\rho$ forces $G$ to be abelian, contradicting condition 2 of $h_G$ ; so for $N \le 1$ the hypotheses cannot all hold and the statement is vacuously true. The theorem itself places no lower bound on $N$ ; it simply quantifies over all $N$ .

2. Conclusion (what is asserted to exist)

Under these hypotheses the theorem asserts that there exist

a sequence of real numbers $\beta : \mathbb{N} \to \mathbb{R}$ ,
a sequence of natural numbers $L : \mathbb{N} \to \mathbb{N}$ ,
a function $Z : \mathbb{N} \to \mathrm{Loop}_4 \to \mathbb{R}$ (a real number $Z_k(\gamma)$ for each index $k$ and each loop $\gamma$ ),
a function $W : \mathrm{List}(\mathrm{Loop}_4) \to \mathbb{C}$ (a complex number $W(A)$ for every finite list $A$ of loops — lists are ordered and may contain repeats),

such that all five of the following hold:

\text{(I) } \mathrm{IsContinuumLimit}_\rho(\beta, L, Z, W),\quad \text{(II) } \mathrm{IsLatticeInvariant}(W),\quad \text{(III) } \mathrm{IsReflectionPositive}(W),

\text{(IV) } \exists\, \Delta \in \mathbb{R},\ 0 < \Delta \ \wedge\ \mathrm{HasMassGap}(W, \Delta),\quad \text{(V) } \mathrm{HasFiniteMass}(W).

Everything is in dimension $d = 4$ : coordinates are indexed by $\{0,1,2,3\}$ , and index $0$ plays the role of "time" in (III), (IV), (V). The existence claim is a plain $\exists$ (not unique existence). All five custom predicates are unfolded below.

3. The lattice objects

Sites, boxes, edges, plaquettes. A site is a point $x \in \mathbb{Z}^4$ (a function $\{0,1,2,3\} \to \mathbb{Z}$ ). $e_\mu$ denotes the unit vector in direction $\mu$ . For $R \in \mathbb{N}$ the box $\Lambda_R = \{x \in \mathbb{Z}^4 : -R \le x_\mu \le R \text{ for all } \mu\}$ (for $R=0$ it is $\{0\}$ ). An edge is a pair $(x,\mu)$ with $x$ a site and $\mu$ a direction, thought of as the segment from $x$ to $x + e_\mu$ . The box edges $E_R$ are the edges $(x,\mu)$ with $x \in \Lambda_R$ and $x + e_\mu \in \Lambda_R$ . A plaquette is a triple $(x,\mu,\nu)$ ; the box plaquettes $P_R$ are those with $x \in \Lambda_R$ , $\mu < \nu$ (as indices), and $x+e_\mu,\ x+e_\nu,\ x+e_\mu+e_\nu \in \Lambda_R$ .

Configurations and links. A configuration on the box of size $R$ is a function $U : E_R \to G$ . For an arbitrary edge $e$ (inside the box or not) the link variable is

\mathrm{link}_U(e) = \begin{cases} U(e) & e \in E_R,\\ 1_G & e \notin E_R,\end{cases}

so every edge outside the box carries the identity element.

Plaquette variable. For $p = (x,\mu,\nu)$ ,

\mathrm{plaq}_U(x,\mu,\nu) = \mathrm{link}_U(x,\mu)\cdot \mathrm{link}_U(x+e_\mu,\nu)\cdot \mathrm{link}_U(x+e_\nu,\mu)^{-1}\cdot \mathrm{link}_U(x,\nu)^{-1}.

Wilson action. With $\operatorname{tr}$ the matrix trace and $\mathrm{Re}$ the real part,

S_\rho(U) = \sum_{p \in P_R} \mathrm{Re}\,\operatorname{tr}\big(\rho(\mathrm{plaq}_U(p))\big) \in \mathbb{R}.

There is no coupling constant inside $S_\rho$ , no subtraction of a constant, and no sign flip; the Gibbs weight is $g_\beta(U) = \exp\big(\beta\, S_\rho(U)\big)$ with the sign $+\beta S_\rho$ .

Haar probability measure and configuration measure. $\mathrm{haarProb}(G)$ is Mathlib's left Haar measure on $G$ built from the positive compact set $G$ itself (the top element of PositiveCompacts G, which exists because $G$ is compact and non-empty), normalised so that $G$ has measure $1$ . The configuration measure $\mu_R$ on $\{U : E_R \to G\}$ is the finite product measure $\bigotimes_{e \in E_R} \mathrm{haarProb}(G)$ (Mathlib's Measure.pi). When $E_R$ is empty (e.g. $R = 0$ ) there is a single configuration and $\mu_R$ gives it mass $1$ .

Expectation. For $\beta \in \mathbb{R}$ and $F : \{U : E_R\to G\} \to \mathbb{C}$ ,

\langle F\rangle_{R,\beta} = \frac{\displaystyle\int F(U)\, g_\beta(U)\, d\mu_R(U)}{\displaystyle\int g_\beta(U)\, d\mu_R(U)} \in \mathbb{C},

with both integrals being Bochner integrals of complex-valued functions (the real $g_\beta$ is cast into $\mathbb{C}$ ). Two conventions are in force: a Bochner integral of a function that is not integrable (in particular not almost-everywhere strongly measurable) is defined to be $0$ , and division by $0$ in $\mathbb{C}$ yields $0$ . Nothing in the definitions assumes integrability or nonvanishing of the denominator.

4. Paths, loops and their operations

Steps. A step is a pair $s = (\mu, b)$ with $\mu \in \{0,1,2,3\}$ and $b$ a Boolean; its displacement is $\vec s = e_\mu$ if $b = \mathrm{true}$ and $\vec s = -e_\mu$ if $b = \mathrm{false}$ .

Vertices, edges and holonomy of a step list. For a start site $x$ and a list of steps $s_1,\dots,s_n$ , put $x_0 = x$ , $x_i = x_{i-1} + \vec s_i$ . Then

$\mathrm{pathVertices}(x; s_1..s_n) = [x_0, x_1, \dots, x_{n-1}]$ — the starting point of each step; it is the empty list if $n = 0$ , and does not separately include $x_n$ ;
$\mathrm{pathEdges}(x; s_1..s_n)$ is the list whose $i$ -th entry is $(x_{i-1}, \mu_i)$ if $b_i = \mathrm{true}$ and $(x_{i-1} - e_{\mu_i}, \mu_i)$ if $b_i = \mathrm{false}$ (edges are always recorded in their positive orientation);
the holonomy is the ordered product

\mathrm{hol}_U(x; s_1..s_n) = h_1 h_2 \cdots h_n,\qquad h_i = \begin{cases}\mathrm{link}_U(x_{i-1},\mu_i) & b_i = \mathrm{true},\\ \mathrm{link}_U(x_{i-1}-e_{\mu_i},\mu_i)^{-1} & b_i = \mathrm{false},\end{cases}

with $\mathrm{hol}_U(x; []) = 1_G$ .

Loops. A loop $\gamma \in \mathrm{Loop}_4$ is a triple $(\gamma.\mathrm{scale} \in \mathbb{N},\ \gamma.\mathrm{base} \in \mathbb{Z}^4,\ \gamma.\mathrm{steps})$ together with a proof that $\sum_i \vec s_i = 0$ (the displacement returns to the base point). The step list may be empty. Two loops with the same base and steps but different scale are different loops.

Refinement. $\mathrm{refine}(\gamma, j)$ has scale $\gamma.\mathrm{scale} + j$ , base $2^j\cdot\gamma.\mathrm{base}$ , and step list obtained by replacing each step by $2^j$ consecutive copies of itself. $\mathrm{refine}(\gamma,0)$ has the same base and steps as $\gamma$ .

Loop at scale $k$ . $\mathrm{atScale}(\gamma,k) = (\text{base},\text{steps})$ of $\mathrm{refine}(\gamma,\ k \mathbin{\dot-} \gamma.\mathrm{scale})$ , where $\dot-$ is truncated natural-number subtraction: if $k < \gamma.\mathrm{scale}$ then $k \dot- \gamma.\mathrm{scale} = 0$ and $\mathrm{atScale}(\gamma,k)$ is just $(\gamma.\mathrm{base},\gamma.\mathrm{steps})$ — a loop is never coarsened, and for every $k \le \gamma.\mathrm{scale}$ the same unrefined data is returned.

Vertices. $\mathrm{vertices}(\gamma) = \mathrm{pathVertices}(\gamma.\mathrm{base};\gamma.\mathrm{steps})$ (at native scale); $\mathrm{verticesAt}(\gamma,k) = \mathrm{pathVertices}$ of $\mathrm{atScale}(\gamma,k)$ ; $\mathrm{edges}(\gamma) = \mathrm{pathEdges}(\gamma.\mathrm{base};\gamma.\mathrm{steps})$ .

Simple. $\gamma$ is simple iff its step list is non-empty, $\mathrm{vertices}(\gamma)$ has no repeated entries, and $\mathrm{edges}(\gamma)$ has no repeated entries (both at the loop's native scale).

Disjoint. $\gamma_1,\gamma_2$ are disjoint iff, with $m = \max(\gamma_1.\mathrm{scale},\gamma_2.\mathrm{scale})$ , the lists $\mathrm{verticesAt}(\gamma_1,m)$ and $\mathrm{verticesAt}(\gamma_2,m)$ have no common entry.

Admissible list. A list $A$ of loops is admissible iff every loop in $A$ is simple and $A$ is pairwise disjoint in list order (each entry disjoint from every later entry). The empty list is admissible. A list containing the same non-trivial loop twice is not admissible.

Translation. For $j \in \mathbb{N}$ and $v \in \mathbb{Z}^4$ , with $m = \max(\gamma.\mathrm{scale}, j)$ and $\gamma' = \mathrm{refine}(\gamma, m - \gamma.\mathrm{scale})$ :

\mathrm{translate}(\gamma, j, v) = \big(\text{scale } m,\ \text{base } \gamma'.\mathrm{base} + 2^{\,m-j}\, v,\ \text{steps } \gamma'.\mathrm{steps}\big).

(Here $m - \gamma.\mathrm{scale}$ and $m - j$ are genuine, since $m$ is the maximum.) Thus $v$ is a displacement measured in units of the scale- $j$ lattice; if $j \le \gamma.\mathrm{scale}$ the loop is not refined and is shifted by $2^{\gamma.\mathrm{scale}-j}v$ ; if $j > \gamma.\mathrm{scale}$ the loop is first refined to scale $j$ and then shifted by $v$ .

Time translation. $\mathrm{timeTranslate}(\gamma, j, n) = \mathrm{translate}(\gamma, j, n\,e_0)$ for $n \in \mathbb{N}$ (so only non-negative shifts along coordinate $0$ ).

Strictly positive time. $\gamma$ has strictly positive time iff every $x \in \mathrm{vertices}(\gamma)$ (native scale) has $x_0 > 0$ .

Time reflection. Let $\theta(x)_\mu = -x_\mu$ if $\mu = 0$ and $x_\mu$ otherwise. Let $\mathrm{reflectStep}(\mu,b) = (\mu,b)$ if $\mu = 0$ and $(\mu, \neg b)$ otherwise. Then

\mathrm{reflect}(\gamma) = \big(\text{scale } \gamma.\mathrm{scale},\ \text{base } \theta(\gamma.\mathrm{base}),\ \text{steps } \mathrm{reverse}\big(\mathrm{map}\ \mathrm{reflectStep}\ \gamma.\mathrm{steps}\big)\big).

(One checks from the definitions that each reflected step has displacement $-\theta(\vec s)$ , so the reflected loop runs through $\theta$ of the original vertices in reverse order.)

Hyperoctahedral coordinate maps. For a permutation $\sigma$ of $\{0,1,2,3\}$ and a sign pattern $\varepsilon : \{0,1,2,3\} \to \{\mathrm{true},\mathrm{false}\}$ , define $\mathrm{coordMap}_{\sigma,\varepsilon}(x)_\mu = (\pm 1)\, x_{\sigma^{-1}(\mu)}$ with sign $+1$ if $\varepsilon(\mu) = \mathrm{true}$ and $-1$ otherwise; and $\mathrm{mapStep}_{\sigma,\varepsilon}(\mu,b) = \big(\sigma(\mu),\ [b = \varepsilon(\sigma(\mu))]\big)$ (the new Boolean is true exactly when $b$ equals $\varepsilon(\sigma\mu)$ ). Then

\mathrm{mapCoords}(\gamma,\sigma,\varepsilon) = \big(\text{scale } \gamma.\mathrm{scale},\ \text{base } \mathrm{coordMap}_{\sigma,\varepsilon}(\gamma.\mathrm{base}),\ \text{steps } \mathrm{map}\ \mathrm{mapStep}_{\sigma,\varepsilon}\ \gamma.\mathrm{steps}\big).

All $\sigma,\varepsilon$ are allowed, including those that move or reverse the time axis $0$ .

5. Observables

Wilson loop at scale $k$ . $\mathcal{W}_{U,k}(\gamma) = \operatorname{tr}\big(\rho(\mathrm{hol}_U(\mathrm{atScale}(\gamma,k)))\big) \in \mathbb{C}$ , the trace of the $N\times N$ matrix $\rho$ of the holonomy of the scale- $k$ version of $\gamma$ . For the empty step list this is $\operatorname{tr}(\rho(1)) = N$ .

Loop product. $\mathcal{W}_{U,k}(A) = \prod_{\gamma \in A}\mathcal{W}_{U,k}(\gamma)$ over the list (equal to $1$ for $A = []$ ).

Loop correlation. For $k, L \in \mathbb{N}$ , $\beta \in \mathbb{R}$ and a list $A$ ,

C_{k,L,\beta}(A) = \big\langle U \mapsto \mathcal{W}_{U,k}(A)\big\rangle_{R = L\cdot 2^k,\ \beta},

i.e. the expectation of Section 3 on the box $\Lambda_{L 2^k}$ with configuration measure $\mu_{L2^k}$ and weight $\exp(\beta S_\rho)$ . Loops whose scale- $k$ vertices leave the box are still evaluated; their out-of-box edges contribute the identity via $\mathrm{link}$ .

6. The five conjuncts

(I) Continuum limit. $\mathrm{IsContinuumLimit}_\rho(\beta,L,Z,W)$ is the conjunction of:

$\beta_k > 0$ for every $k \in \mathbb{N}$ ;
$Z_k(\gamma) > 0$ for every $k \in \mathbb{N}$ and every loop $\gamma$ ;
$L_k \to \infty$ as $k \to \infty$ (for every $M$ there is $k_0$ with $L_k \ge M$ for all $k \ge k_0$ );
for every admissible list $A$ of loops,

\Big(\prod_{\gamma\in A} Z_k(\gamma)\Big)\cdot C_{k,\,L_k,\,\beta_k}(A) \longrightarrow W(A)\quad\text{in }\mathbb{C}\text{ as } k\to\infty .

Nothing is asserted about $W(A)$ for non-admissible $A$ ; $W$ is unconstrained there by (I). For $A = []$ the convergent quantity is $C_{k,L_k,\beta_k}([]) = \big(\int g_{\beta_k}\,d\mu\big)/\big(\int g_{\beta_k}\,d\mu\big)$ , subject to the $0$ -conventions above.

(II) Lattice invariance. $\mathrm{IsLatticeInvariant}(W)$ is the conjunction of:

for every admissible list $A$ , every $j \in \mathbb{N}$ and every $v \in \mathbb{Z}^4$ : $W\big(\mathrm{map}\ (\gamma \mapsto \mathrm{translate}(\gamma,j,v))\ A\big) = W(A)$ ;
for every admissible list $A$ , every permutation $\sigma$ of $\{0,1,2,3\}$ and every $\varepsilon : \{0,1,2,3\} \to \mathrm{Bool}$ : $W\big(\mathrm{map}\ (\gamma\mapsto\mathrm{mapCoords}(\gamma,\sigma,\varepsilon))\ A\big) = W(A)$ .

Only admissibility of $A$ is required, not of the transformed list.

(III) Reflection positivity. $\mathrm{IsReflectionPositive}(W)$ : for every $n \in \mathbb{N}$ , every $c : \{0,\dots,n-1\} \to \mathbb{C}$ and every family $A_0,\dots,A_{n-1}$ of lists of loops such that each $A_i$ is admissible and every loop in each $A_i$ has strictly positive time, the complex number

S = \sum_{i=0}^{n-1}\sum_{j=0}^{n-1} \overline{c_i}\, c_j\, W\big(\mathrm{map}\ \mathrm{reflect}\ A_i \ {+\!\!+}\ A_j\big)

(where $+\!\!+$ is list concatenation: the reflected loops of $A_i$ followed by the loops of $A_j$ , and $\overline{\,\cdot\,}$ is complex conjugation) satisfies $\mathrm{Im}\,S = 0$ and $0 \le \mathrm{Re}\,S$ . For $n = 0$ the sum is $0$ and the condition holds trivially. The concatenated list is not required to be admissible.

(IV) Mass gap. There exists a real $\Delta > 0$ such that $\mathrm{HasMassGap}(W,\Delta)$ , which means: for every pair of admissible lists $A, B$ there exists a real constant $C$ (depending on $A$ and $B$ only, of arbitrary sign) such that for all $j, n \in \mathbb{N}$ , if the list $A \mathbin{+\!\!+} \mathrm{map}\ (\gamma\mapsto \mathrm{timeTranslate}(\gamma,j,n))\ B$ is admissible, then

\Big\| W\big(A \mathbin{+\!\!+} \mathrm{map}\ (\gamma\mapsto \mathrm{timeTranslate}(\gamma,j,n))\ B\big) - W(A)\,W(B) \Big\| \ \le\ C\cdot \exp\!\Big(-\Delta\cdot \frac{n}{2^{j}}\Big),

with $\|\cdot\|$ the modulus on $\mathbb{C}$ and $n/2^j$ ordinary real division ( $2^j \neq 0$ , so no junk value). Pairs $(j,n)$ for which the concatenated list is not admissible impose no constraint; if no such pair is admissible the requirement on $(A,B)$ is vacuous. The instances $A = []$ or $B = []$ are included (e.g. for $B = []$ the concatenation is $A$ itself and the bound reads $\|W(A) - W(A)W([])\| \le C e^{-\Delta n/2^j}$ for all $j,n$ ).

(V) Finite mass. $\mathrm{HasFiniteMass}(W)$ is literally $\neg\big(\forall \Delta \in \mathbb{R},\ \mathrm{HasMassGap}(W,\Delta)\big)$ ; classically, there is some real $\Delta$ (no sign restriction) for which $\mathrm{HasMassGap}(W,\Delta)$ fails, i.e. there exist admissible $A, B$ such that for every real $C$ there are $j, n \in \mathbb{N}$ with $A \mathbin{+\!\!+} \mathrm{map}\ (\gamma\mapsto\mathrm{timeTranslate}(\gamma,j,n))\ B$ admissible and

\Big\| W\big(A \mathbin{+\!\!+} \mathrm{map}\ (\gamma\mapsto \mathrm{timeTranslate}(\gamma,j,n))\ B\big) - W(A)\,W(B) \Big\| \ >\ C\cdot \exp\!\Big(-\Delta\cdot \frac{n}{2^{j}}\Big).

7. Summary in one sentence

For every compact Hausdorff topological group $G$ (with Borel $\sigma$ -algebra) that is connected, non-abelian, and has every closed normal subgroup finite or everything, and every $N\in\mathbb{N}$ and continuous injective homomorphism $\rho : G\to \mathrm{U}(N)$ , there exist sequences $\beta_k \in \mathbb{R}$ , $L_k \in \mathbb{N}$ , normalisations $Z_k(\gamma)\in\mathbb{R}$ and a function $W$ on lists of loops in $\mathbb{Z}^4$ such that: $\beta_k>0$ , $Z_k>0$ , $L_k\to\infty$ , and for each admissible list $A$ the rescaled Wilson-loop expectations $\prod_{\gamma\in A}Z_k(\gamma)\cdot C_{k,L_k,\beta_k}(A)$ (finite-box lattice expectations on $\Lambda_{L_k 2^k}$ with product-Haar measure and weight $e^{+\beta_k S_\rho}$ , loops refined to scale $k$ ) converge to $W(A)$ ; $W$ is invariant on admissible lists under the translation and coordinate-map operations of Section 4; $W$ satisfies the reflection-positivity inequality (III) for strictly-positive-time admissible families; there is some $\Delta>0$ with the exponential clustering bound (IV); and it is not the case that (IV) holds for every real $\Delta$ .

View graph

Yang–Mills existence and mass gap on R4\mathbb{R}^4R4 for any compact simple gauge group (Clay Millennium Prize Problem, lattice formulation of Jaffe–Witten §6.5)

Read-back: YangMills.existence_and_mass_gap