Wilson lattice Yang–Mills theory with compact simple gauge group: gauge fields, Wilson loops, dyadic loops, and the axioms for a continuum theory with a mass gap (Jaffe–Witten §4, §6.5)

Definition

YangMills

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

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

This bundle fixes, in the namespace YangMills, the objects needed to state the Yang–Mills existence and mass gap problem of Jaffe–Witten in the precise form given by Wilson's lattice approximation (Jaffe–Witten §6.5; Osterwalder–Seiler 1978; Chatterjee 2019): a compact simple gauge group, Wilson's lattice gauge theory on finite boxes, Wilson loop observables on dyadic loops, the lattice symmetries, and the properties demanded of a continuum theory.

Gauge group. A compact Hausdorff topological group $G$ is a compact simple gauge group (IsCompactSimpleGaugeGroup G) when it is connected, non-abelian, and every closed normal subgroup is finite or equal to $G$ . For a compact connected Lie group this is equivalent to its Lie algebra being simple (a finite centre is allowed). $G$ is always used together with a homomorphism $\rho : G \to U(N)$ into the unitary group of $\mathbb{C}^N$ ; in the goal $\rho$ is continuous and injective, which makes $G$ a compact Lie group.

Lattice, box, gauge fields. Sites are $x \in \mathbb{Z}^d$ (Site d), $e_\mu$ is the unit vector (unit d μ), and the box of radius $R$ is $\{x : |x_\mu| \le R\ \forall \mu\}$ (box d R). An edge is a pair $(x,\mu)$ , representing the segment from $x$ to $x+e_\mu$ ; boxEdges d R are the edges with both endpoints in the box, boxPlaquettes d R the plaquettes $(x,\mu,\nu)$ , $\mu<\nu$ , with all four corners $x, x+e_\mu, x+e_\nu, x+e_\mu+e_\nu$ in the box. A gauge field (Config d R G) assigns $U(x,\mu) \in G$ to every edge of the box; link U e returns $U(e)$ for edges of the box and the junk value $1$ otherwise. The plaquette holonomy is $U_p = U(x,\mu)\,U(x+e_\mu,\nu)\,U(x+e_\nu,\mu)^{-1}\,U(x,\nu)^{-1}$ (plaquette), a gauge transformation $g : \mathbb{Z}^d \to G$ acts by $U(x,\mu) \mapsto g(x)\,U(x,\mu)\,g(x+e_\mu)^{-1}$ (gaugeTransform), and the Wilson action is $S(U) = \sum_{p \in \text{boxPlaquettes}} \operatorname{Re}\operatorname{tr}\rho(U_p) \qquad\text{(`wilsonAction ρ U`)}.$

Measure and expectation. haarProb G is the Haar probability measure of the compact group $G$ , configMeasure d R G its product over the edges of the box, gibbsWeight ρ β U $= e^{\beta S(U)}$ , and $\langle F \rangle_{R,\beta} = \frac{\int F(U)\,e^{\beta S(U)}\,dU}{\int e^{\beta S(U)}\,dU} \qquad\text{(`expectation ρ β F`)}$ is the expectation of a complex observable $F$ in the Wilson lattice gauge theory on the box with free boundary conditions. plaquetteMeasure ρ β is the probability measure $e^{\beta\operatorname{Re}\operatorname{tr}\rho(g)}\,dg / \int e^{\beta\operatorname{Re}\operatorname{tr}\rho}\,dg$ on $G$ .

Paths and dyadic loops. A step is $(\mu, b)$ with displacement $+e_\mu$ ( $b = \mathrm{true}$ ) or $-e_\mu$ (stepVec). pathVertices x s lists the vertices $v_0 = x, v_1, \dots, v_{m-1}$ of the path with steps $s$ (the endpoint $v_m$ is omitted), pathEdges its undirected edges as (lower endpoint, direction), and pathHol U x s is the ordered product of the link variables along the path, a step $-e_\mu$ from $x$ contributing $U(x-e_\mu,\mu)^{-1}$ . A dyadic loop (Loop d) is a scale $k_0$ , a base point and a list of steps whose displacements sum to zero (the closed field); its integer vertices $v$ stand for the physical points $2^{-k_0}v$ . Loop.refine γ j reads the same physical loop $j$ scales finer (base point times $2^j$ , every step subdivided into $2^j$ steps); Loop.atScale γ k is the path representing $\gamma$ at scale $k$ (for $k < k_0$ it is the data of $\gamma$ unchanged, a junk interpretation that never enters a limit $k \to \infty$ ). Loop.vertices, Loop.edges are the vertices and edges at the loop's own scale, Loop.verticesAt γ k the vertices at scale $k$ ; Loop.IsSimple γ means non-empty with no repeated vertex and no repeated edge; Loop.Disjoint γ₁ γ₂ means the two loops share no vertex when read at the finer of their two scales (equivalently, they are disjoint subsets of $\mathbb{R}^d$ ); Loop.InBox γ k R means all vertices at scale $k$ lie in the box of radius $R$ . Loop.rect k T R μ ν is the rectangle with corner $0$ , $T$ steps in direction $\mu$ and $R$ steps in direction $\nu$ , at scale $k$ .

Symmetries. Loop.translate γ j v is the translate by $2^{-j}v$ ; Loop.timeTranslate γ j n the translate by $n\,2^{-j}$ in the time direction $0$ ; Loop.PositiveTime / Loop.StrictlyPositiveTime say all vertices have time coordinate $\ge 0$ / $> 0$ ; Loop.reflect γ is the Osterwalder–Schrader reflection: time coordinate negated (timeFlip) and orientation reversed, so that for unitary $\rho$ , $\operatorname{tr}\rho(U_{\mathrm{reflect}\,\gamma}) = \overline{\operatorname{tr}\rho(U_{\theta\gamma})}$ ; Loop.mapCoords γ σ ε is the image under the signed coordinate permutation $x \mapsto (\varepsilon_\mu x_{\sigma^{-1}\mu})_\mu$ of the hypercubic group.

Wilson loops and correlation functions. wilsonLoop ρ U k γ $= \operatorname{tr}\rho(U_\gamma)$ with $\gamma$ read at scale $k$ ; loopProduct ρ U k A $= \prod_{\gamma \in A}\operatorname{tr}\rho(U_\gamma)$ ; and $\langle A \rangle_{k,L,\beta} = \Big\langle \prod_{\gamma \in A}\operatorname{tr}\rho(U_\gamma) \Big\rangle_{L 2^k,\ \beta} \qquad\text{(`loopCorrelation ρ k L β A`)}$ is the correlation function of the family $A$ at lattice spacing $2^{-k}$ in the box of physical half-side $L$ (lattice radius $L\cdot 2^k$ ). A family $A$ is admissible (IsAdmissible A) when every loop is simple and the loops are pairwise disjoint.

Axioms for a continuum theory $W$ (a function from lists of loops to $\mathbb{C}$ ):

IsContinuumLimit ρ β L Z W: $\beta_k > 0$ , $Z_k(\gamma) > 0$ , $L_k \to \infty$ , and for every admissible $A$ , $\prod_{\gamma\in A} Z_k(\gamma)\cdot\langle A\rangle_{k,L_k,\beta_k} \to W(A)$ as $k \to \infty$ (continuum and infinite-volume limit after multiplicative renormalization of each loop);
IsLatticeInvariant W: $W$ is invariant under all dyadic translations and all signed coordinate permutations, on admissible families;
IsReflectionPositive W: 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$ ;
HasMassGap W Δ: for all admissible $A, B$ there is $C$ such that $|W(A \cup \tau_t B) - W(A)W(B)| \le C e^{-\Delta t}$ for every dyadic $t = n/2^j \ge 0$ for which $A \cup \tau_t B$ is admissible ( $\tau_t$ = time translation by $t$ );
HasFiniteMass W: it is not the case that $W$ has mass gap $\Delta$ for every $\Delta$ — Jaffe–Witten's "the supremum of such $\Delta$ is the mass $m$ , and we require $m < \infty$ ".

Formalization Note Jaffe–Witten give no formal definition of "quantum Yang–Mills theory"; this bundle follows their §6.5 and the constructive literature by defining the theory through the limits of Wilson-loop correlation functions of Wilson's lattice theory. Under Osterwalder–Schrader reconstruction from a reflection-positive $W$ , exponential decay of all connected time-translated correlations at rate $\Delta$ is equivalent to the Hamiltonian having no spectrum in $(0,\Delta)$ , so HasMassGap is Jaffe–Witten's mass gap in Euclidean form. Multiplicative renormalization constants are needed because raw Wilson loop expectations are expected to vanish in the continuum limit (perimeter divergence); they rescale connected correlations but cannot create time dependence. Only lattice symmetries (dyadic translations, hypercubic group, time reflection) can be imposed on axis-parallel loops; full Euclidean invariance and smeared field operators are not encoded. All integrals are Bochner integrals for the product Haar measure; the integrands are continuous on a compact space and the partition function is positive, so no junk value arises there. Edges outside the box carry the value $1$ , and a loop read at a scale coarser than its own is read unchanged; fixed-scale theorems carry the hypothesis γ.scale ≤ k.

Definition code

import Mathlib

/-!
A. Jaffe, E. Witten, *Quantum Yang–Mills theory*, Clay Mathematics Institute Millennium Prize
Problem description (2000), §4 "The Problem" (p. 6) and §6.5 "Yang–Mills theory" (p. 11).

The objects needed to state the Yang–Mills existence and mass gap problem in the form made
precise by Wilson's lattice approximation (Jaffe–Witten §6.5; K. Osterwalder and E. Seiler,
Ann. Phys. 110 (1978); S. Chatterjee, *Yang–Mills for probabilists*, 2019):

* a **compact simple gauge group** `G`, presented with a faithful finite-dimensional unitary
  representation `ρ : G →* U(N)` (every compact Lie group has one, and a compact group with one is
  a Lie group);
* the **Wilson lattice gauge theory** on the finite lattice `{x ∈ ℤ^d : |x_μ| ≤ R}` with free
  boundary conditions: link variables `U(x, μ) ∈ G`, plaquette holonomies, the Wilson action
  `∑_p Re tr ρ(U_p)`, the product Haar probability measure, and the expectation
  `⟨F⟩ = ∫ F e^{β ∑_p Re tr ρ(U_p)} / ∫ e^{β ∑_p Re tr ρ(U_p)}` at inverse coupling `β`;
* **Wilson loops** `tr ρ(U_γ)`, where `γ` is an axis-parallel closed lattice path with dyadic
  vertices ("dyadic loop"), read at lattice spacing `2^{-k}`; their correlation functions in the
  box of physical half-side `L`;
* the symmetries of the lattice (dyadic translations, coordinate permutations and reflections,
  Osterwalder–Schrader time reflection) acting on loops;
* the axioms imposed on a **continuum theory** `W` (a correlation functional on families of
  loops): being the continuum/infinite-volume limit of the lattice theories after a multiplicative
  renormalization of each loop, lattice Euclidean invariance, reflection positivity, and the
  **mass gap** in Euclidean form (exponential clustering in the time direction), together with
  Jaffe–Witten's requirement that the mass `m = sup Δ` be finite.

Conventions.  `Site d = ℤ^d` are lattice sites, direction `0 : Fin d` is Euclidean time.  A
`Loop d` carries its own scale `k₀`: its integer data describe the physical loop with lattice
spacing `2^{-k₀}`; at a finer scale `k ≥ k₀` it is read by scaling the base point by `2^{k-k₀}`
and subdividing every step into `2^{k-k₀}` unit steps (`Loop.atScale`).  For `k < k₀`,
`Loop.atScale` returns the coarse data unchanged (a junk interpretation that never matters for
limits `k → ∞`; fixed-scale statements carry the hypothesis `γ.scale ≤ k`).  Link variables of
edges outside the box are the junk value `1`.
-/

namespace YangMills

noncomputable section

open MeasureTheory Filter Topology TopologicalSpace

/-! ### The gauge group -/

/-- `G` is a compact simple gauge group in the sense of Jaffe–Witten: connected, non-abelian, and
with no closed normal subgroups other than finite ones and `G` itself.  For a compact Lie group
(which `G` is, as soon as it has a faithful finite-dimensional continuous representation) this is
equivalent to: `G` is connected and its Lie algebra is simple; it allows a finite centre (e.g.
`SU(N)`, `Spin(N)`, `G₂`, …) and excludes tori, `U(N)`, `SO(4)`, and all products. -/
structure IsCompactSimpleGaugeGroup (G : Type*) [Group G] [TopologicalSpace G] : Prop where
  connected : ConnectedSpace G
  nonabelian : ∃ a b : G, a * b ≠ b * a
  normal_finite_or_top : ∀ K : Subgroup G, K.Normal → IsClosed (K : Set G) →
    (K : Set G).Finite ∨ K = ⊤

/-! ### The lattice -/

/-- Lattice sites: `ℤ^d`. -/
abbrev Site (d : ℕ) := Fin d → ℤ

/-- The unit vector `e_μ`. -/
def unit (d : ℕ) (μ : Fin d) : Site d := Pi.single μ 1

/-- The box `{x ∈ ℤ^d : |x_μ| ≤ R for all μ}`. -/
def box (d : ℕ) (R : ℕ) : Finset (Site d) :=
  Fintype.piFinset fun _ => Finset.Icc (-(R : ℤ)) R

/-- A directed edge `(x, μ)` of `ℤ^d`, from `x` to `x + e_μ`. -/
abbrev Edge (d : ℕ) := Site d × Fin d

/-- The edges with both endpoints in the box. -/
def boxEdges (d R : ℕ) : Finset (Edge d) :=
  (box d R ×ˢ Finset.univ).filter fun e => e.1 + unit d e.2 ∈ box d R

/-- A plaquette `(x, μ, ν)`: the unit square with corners `x, x+e_μ, x+e_μ+e_ν, x+e_ν`. -/
abbrev Plaquette (d : ℕ) := Site d × Fin d × Fin d

/-- The plaquettes `(x, μ, ν)` with `μ < ν` and all four corners in the box. -/
def boxPlaquettes (d R : ℕ) : Finset (Plaquette d) :=
  (box d R ×ˢ (Finset.univ ×ˢ Finset.univ)).filter fun p =>
    p.2.1 < p.2.2 ∧ p.1 + unit d p.2.1 ∈ box d R ∧ p.1 + unit d p.2.2 ∈ box d R ∧
      p.1 + unit d p.2.1 + unit d p.2.2 ∈ box d R

/-- A lattice gauge field on the box: one group element per edge of the box. -/
abbrev Config (d R : ℕ) (G : Type*) := boxEdges d R → G

section Lattice

variable {d R : ℕ} {G : Type*} [Group G]

/-- The link variable `U(x, μ)` of an edge; edges outside the box carry the junk value `1`. -/
def link (U : Config d R G) (e : Edge d) : G :=
  if h : e ∈ boxEdges d R then U ⟨e, h⟩ else 1

/-- The plaquette holonomy `U_p = U(x,μ) U(x+e_μ,ν) U(x+e_ν,μ)⁻¹ U(x,ν)⁻¹`. -/
def plaquette (U : Config d R G) (p : Plaquette d) : G :=
  link U (p.1, p.2.1) * link U (p.1 + unit d p.2.1, p.2.2) *
    (link U (p.1 + unit d p.2.2, p.2.1))⁻¹ * (link U (p.1, p.2.2))⁻¹

/-- A gauge transformation `g : ℤ^d → G` acts by `U(x,μ) ↦ g(x) U(x,μ) g(x+e_μ)⁻¹`. -/
def gaugeTransform (g : Site d → G) (U : Config d R G) : Config d R G :=
  fun e => g e.1.1 * U e * (g (e.1.1 + unit d e.1.2))⁻¹

variable {N : ℕ} (ρ : G →* Matrix.unitaryGroup (Fin N) ℂ)

/-- The Wilson action `S(U) = ∑_{p ⊆ box} Re tr ρ(U_p)` (the Gibbs density is `e^{β S}`). -/
noncomputable def wilsonAction (U : Config d R G) : ℝ :=
  ∑ p ∈ boxPlaquettes d R, (Matrix.trace (ρ (plaquette U p) : Matrix (Fin N) (Fin N) ℂ)).re

end Lattice

section Measure

variable {d R : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [MeasurableSpace G] [BorelSpace G]

/-- The Haar probability measure of the compact group `G`. -/
noncomputable def haarProb (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : Measure G :=
  Measure.haarMeasure (⊤ : PositiveCompacts G)

/-- The product Haar probability measure on the gauge fields of the box. -/
noncomputable def configMeasure (d R : ℕ) (G : Type*) [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    Measure (Config d R G) :=
  Measure.pi fun _ => haarProb G

variable {N : ℕ} (ρ : G →* Matrix.unitaryGroup (Fin N) ℂ)

/-- The Gibbs weight `e^{β S(U)}` of the Wilson lattice gauge theory at inverse coupling `β`. -/
noncomputable def gibbsWeight (β : ℝ) (U : Config d R G) : ℝ :=
  Real.exp (β * wilsonAction ρ U)

/-- The expectation `⟨F⟩_{R,β} = ∫ F e^{βS} dU / ∫ e^{βS} dU` of an observable `F` in the
Wilson lattice gauge theory on the box of radius `R`, with free boundary conditions. -/
noncomputable def expectation (β : ℝ) (F : Config d R G → ℂ) : ℂ :=
  (∫ U, F U * (gibbsWeight ρ β U : ℂ) ∂configMeasure d R G) /
    ∫ U, (gibbsWeight ρ β U : ℂ) ∂configMeasure d R G

/-- The single-plaquette probability measure `e^{β Re tr ρ(g)} dg / ∫ e^{β Re tr ρ} dg` on `G`
(used in the exact solution of the two-dimensional theory). -/
noncomputable def plaquetteMeasure (β : ℝ) : Measure G :=
  (ENNReal.ofReal (∫ g, Real.exp (β * (Matrix.trace (ρ g : Matrix (Fin N) (Fin N) ℂ)).re)
      ∂haarProb G))⁻¹ •
    (haarProb G).withDensity fun g =>
      ENNReal.ofReal (Real.exp (β * (Matrix.trace (ρ g : Matrix (Fin N) (Fin N) ℂ)).re))

end Measure

/-! ### Paths and loops -/

/-- A unit step `(μ, b)`: `+e_μ` if `b = true`, `-e_μ` if `b = false`. -/
abbrev Step (d : ℕ) := Fin d × Bool

/-- The displacement of a step. -/
def stepVec {d : ℕ} (s : Step d) : Site d := if s.2 then unit d s.1 else -unit d s.1

section Paths

variable {d : ℕ}

/-- The vertices `x = v₀, v₁, …, v_{m-1}` of the path starting at `x` with steps `s₁, …, s_m`
(the final endpoint `v_m` is not listed; for a closed path it is `v₀`). -/
def pathVertices : Site d → List (Step d) → List (Site d)
  | _, [] => []
  | x, s :: rest => x :: pathVertices (x + stepVec s) rest

/-- The undirected edges of a path, each written as `(lower endpoint, direction)`. -/
def pathEdges : Site d → List (Step d) → List (Edge d)
  | _, [] => []
  | x, s :: rest => (if s.2 then (x, s.1) else (x - unit d s.1, s.1)) :: pathEdges (x + stepVec s) rest

variable {R : ℕ} {G : Type*} [Group G]

/-- The holonomy (ordered product of link variables) along the path from `x` with steps `s`;
a step `-e_μ` from `x` contributes `U(x - e_μ, μ)⁻¹`. -/
def pathHol (U : Config d R G) : Site d → List (Step d) → G
  | _, [] => 1
  | x, s :: rest =>
    (if s.2 then link U (x, s.1) else (link U (x - unit d s.1, s.1))⁻¹) *
      pathHol U (x + stepVec s) rest

end Paths

/-- A dyadic loop: an axis-parallel closed lattice path, read at lattice spacing `2^{-scale}`.
Its physical vertices are `2^{-scale} · v` for the vertices `v` of the path. -/
structure Loop (d : ℕ) where
  /-- the scale `k₀`: the loop lives on the lattice `2^{-k₀} ℤ^d` -/
  scale : ℕ
  /-- the starting vertex, in lattice units at scale `k₀` -/
  base : Site d
  /-- the unit steps -/
  steps : List (Step d)
  /-- the path returns to its starting vertex -/
  closed : (steps.map stepVec).sum = 0

namespace Loop

variable {d : ℕ}

theorem sum_map_stepVec_flatMap_replicate (n : ℕ) (l : List (Step d)) :
    ((l.flatMap (List.replicate n)).map stepVec).sum = n • (l.map stepVec).sum := by
  induction l with
  | nil => simp
  | cons s l ih =>
    simp only [List.flatMap_cons, List.map_append, List.sum_append, List.map_replicate,
      List.sum_replicate, List.map_cons, List.sum_cons, ih, smul_add]

/-- The same physical loop read `j` scales finer: base point scaled by `2^j`, each step
subdivided into `2^j` unit steps. -/
def refine (γ : Loop d) (j : ℕ) : Loop d where
  scale := γ.scale + j
  base := (2 ^ j : ℤ) • γ.base
  steps := γ.steps.flatMap (List.replicate (2 ^ j))
  closed := by rw [sum_map_stepVec_flatMap_replicate, γ.closed, smul_zero]

/-- The lattice path (base point, steps) representing `γ` at scale `k`; meaningful for
`k ≥ γ.scale` (for `k < γ.scale` it returns the data of `γ` unchanged). -/
def atScale (γ : Loop d) (k : ℕ) : Site d × List (Step d) :=
  ((γ.refine (k - γ.scale)).base, (γ.refine (k - γ.scale)).steps)

/-- The vertices of `γ` at its own scale (each listed once for a simple loop). -/
def vertices (γ : Loop d) : List (Site d) := pathVertices γ.base γ.steps

/-- The vertices of `γ` read at scale `k`. -/
def verticesAt (γ : Loop d) (k : ℕ) : List (Site d) :=
  pathVertices (γ.atScale k).1 (γ.atScale k).2

/-- The undirected edges of `γ` at its own scale. -/
def edges (γ : Loop d) : List (Edge d) := pathEdges γ.base γ.steps

/-- `γ` is a simple closed curve: non-empty, visits no vertex twice, traverses no edge twice. -/
def IsSimple (γ : Loop d) : Prop := γ.steps ≠ [] ∧ γ.vertices.Nodup ∧ γ.edges.Nodup

/-- Two dyadic loops are disjoint as subsets of `ℝ^d`: read at the finer of their two scales,
they share no vertex. -/
def Disjoint (γ₁ γ₂ : Loop d) : Prop :=
  List.Disjoint (γ₁.verticesAt (max γ₁.scale γ₂.scale)) (γ₂.verticesAt (max γ₁.scale γ₂.scale))

/-- All vertices of `γ` (read at scale `k`) lie in the box of radius `R`. -/
def InBox (γ : Loop d) (k R : ℕ) : Prop := ∀ x ∈ γ.verticesAt k, x ∈ box d R

/-- Translation of `γ` by the dyadic vector `2^{-j} v`. -/
def translate (γ : Loop d) (j : ℕ) (v : Site d) : Loop d where
  scale := max γ.scale j
  base := (γ.refine (max γ.scale j - γ.scale)).base + (2 ^ (max γ.scale j - j) : ℤ) • v
  steps := (γ.refine (max γ.scale j - γ.scale)).steps
  closed := (γ.refine (max γ.scale j - γ.scale)).closed

section Time

variable [NeZero d]

/-- Translation of `γ` forward in Euclidean time (direction `0`) by `n · 2^{-j}`. -/
def timeTranslate (γ : Loop d) (j n : ℕ) : Loop d := γ.translate j ((n : ℤ) • unit d 0)

/-- All vertices of `γ` have time coordinate `≥ 0`. -/
def PositiveTime (γ : Loop d) : Prop := ∀ x ∈ γ.vertices, 0 ≤ x 0

/-- All vertices of `γ` have time coordinate `> 0`. -/
def StrictlyPositiveTime (γ : Loop d) : Prop := ∀ x ∈ γ.vertices, 0 < x 0

/-- Time reflection `(x₀, x⃗) ↦ (-x₀, x⃗)` on sites. -/
def timeFlip (x : Site d) : Site d := fun μ => if μ = 0 then -x μ else x μ

theorem timeFlip_add (x y : Site d) : timeFlip (x + y) = timeFlip x + timeFlip y := by
  funext μ; simp only [timeFlip, Pi.add_apply]; split_ifs <;> ring

theorem timeFlip_zero : timeFlip (0 : Site d) = 0 := by
  funext μ; simp [timeFlip]

/-- Time reflection as an additive map. -/
def timeFlipHom : Site d →+ Site d where
  toFun := timeFlip
  map_zero' := timeFlip_zero
  map_add' := timeFlip_add

/-- The step of the reflected-and-reversed loop: time steps keep their sign, spatial steps flip. -/
def reflectStep (s : Step d) : Step d := if s.1 = 0 then s else (s.1, !s.2)

theorem stepVec_reflectStep (s : Step d) : stepVec (reflectStep s) = -timeFlip (stepVec s) := by
  obtain ⟨μ, b⟩ := s
  funext ν
  simp only [reflectStep, stepVec, timeFlip, unit, Pi.neg_apply]
  by_cases hμ : μ = 0 <;> by_cases hν : ν = 0 <;> cases b <;>
    simp [hμ, hν, Pi.single_apply]

theorem sum_map_stepVec_reflect (l : List (Step d)) :
    (((l.map reflectStep).reverse).map stepVec).sum = -timeFlip (l.map stepVec).sum := by
  induction l with
  | nil => simp [timeFlip_zero]
  | cons s l ih =>
    simp only [List.map_cons, List.reverse_cons, List.map_append, List.sum_append, ih,
      List.map_nil, List.sum_cons, List.sum_nil, add_zero, stepVec_reflectStep, timeFlip_add]
    abel

/-- The Osterwalder–Schrader reflection of a loop: reflect the time coordinate and reverse the
orientation, so that `tr ρ(U_{reflect γ}) = conj (tr ρ(U_{θγ}))` for unitary `ρ`. -/
def reflect (γ : Loop d) : Loop d where
  scale := γ.scale
  base := timeFlip γ.base
  steps := (γ.steps.map reflectStep).reverse
  closed := by rw [sum_map_stepVec_reflect, γ.closed, timeFlip_zero, neg_zero]

end Time

section Hyperoctahedral

/-- The signed coordinate permutation `x ↦ (ε_μ · x_{σ⁻¹ μ})_μ` of `ℤ^d`, where `ε_μ = ±1`
according to `ε μ = true / false`. -/
def coordMap (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) (x : Site d) : Site d :=
  fun μ => (if ε μ then 1 else -1) * x (σ.symm μ)

theorem coordMap_add (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) (x y : Site d) :
    coordMap σ ε (x + y) = coordMap σ ε x + coordMap σ ε y := by
  funext μ; simp only [coordMap, Pi.add_apply]; ring

theorem coordMap_zero (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) :
    coordMap σ ε (0 : Site d) = 0 := by
  funext μ; simp [coordMap]

/-- The signed coordinate permutation as an additive map. -/
def coordMapHom (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) : Site d →+ Site d where
  toFun := coordMap σ ε
  map_zero' := coordMap_zero σ ε
  map_add' := coordMap_add σ ε

/-- The image of a step under a signed coordinate permutation. -/
def mapStep (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) (s : Step d) : Step d :=
  (σ s.1, s.2 == ε (σ s.1))

theorem stepVec_mapStep (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) (s : Step d) :
    stepVec (mapStep σ ε s) = coordMap σ ε (stepVec s) := by
  obtain ⟨μ, b⟩ := s
  funext ν
  simp only [mapStep, stepVec, coordMap, unit]
  by_cases hν : ν = σ μ
  · subst hν
    simp only [Equiv.symm_apply_apply]
    cases b <;> by_cases hε : ε (σ μ) = true <;> simp [hε]
  · have h1 : σ.symm ν ≠ μ := fun h => hν (by rw [← h, Equiv.apply_symm_apply])
    have h2 : (Pi.single (σ μ) (1 : ℤ) : Site d) ν = 0 := Pi.single_eq_of_ne hν 1
    have h3 : (Pi.single μ (1 : ℤ) : Site d) (σ.symm ν) = 0 := Pi.single_eq_of_ne h1 1
    cases b <;> by_cases hε : ε (σ μ) = true <;> simp [hε, h2, h3]

/-- The image of `γ` under the signed coordinate permutation `(σ, ε)` of the hypercubic group. -/
def mapCoords (γ : Loop d) (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool) : Loop d where
  scale := γ.scale
  base := coordMap σ ε γ.base
  steps := γ.steps.map (mapStep σ ε)
  closed := by
    rw [List.map_map]
    have h1 : (stepVec ∘ mapStep σ ε) = fun s : Step d => coordMapHom σ ε (stepVec s) := by
      funext s; simp [stepVec_mapStep, coordMapHom]
    rw [h1]
    have h2 : (fun s : Step d => coordMapHom σ ε (stepVec s)) = (coordMapHom σ ε) ∘ stepVec := rfl
    rw [h2, ← List.map_map, ← map_list_sum, γ.closed, map_zero]

end Hyperoctahedral

/-- The rectangular loop with corner `0`, extending `T` lattice units in direction `μ` and `R`
in direction `ν`, at scale `k` (so of physical size `2^{-k} T × 2^{-k} R`). -/
def rect (k T R : ℕ) (μ ν : Fin d) : Loop d where
  scale := k
  base := 0
  steps := List.replicate T (μ, true) ++ List.replicate R (ν, true) ++
    List.replicate T (μ, false) ++ List.replicate R (ν, false)
  closed := by
    simp only [List.map_append, List.sum_append, List.map_replicate, List.sum_replicate, stepVec,
      Bool.false_eq_true, ↓reduceIte, smul_neg]
    abel

end Loop

/-! ### Wilson loops and their correlation functions -/

section Observables

variable {d R N : ℕ} {G : Type*} [Group G] (ρ : G →* Matrix.unitaryGroup (Fin N) ℂ)

/-- The Wilson loop `W_γ(U) = tr ρ(U_γ)`, the trace of the holonomy of `U` around `γ` read at
scale `k`. -/
noncomputable def wilsonLoop (U : Config d R G) (k : ℕ) (γ : Loop d) : ℂ :=
  Matrix.trace (ρ (pathHol U (γ.atScale k).1 (γ.atScale k).2) : Matrix (Fin N) (Fin N) ℂ)

/-- The product `∏_{γ ∈ A} W_γ(U)` over a family of loops. -/
noncomputable def loopProduct (U : Config d R G) (k : ℕ) (A : List (Loop d)) : ℂ :=
  (A.map (wilsonLoop ρ U k)).prod

variable [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G]
  [BorelSpace G]

/-- The correlation function `⟨∏_{γ ∈ A} tr ρ(U_γ)⟩_{k,L,β}` of a family of dyadic loops in the
Wilson lattice gauge theory at lattice spacing `2^{-k}`, in the box of physical half-side `L`
(lattice radius `L · 2^k`), at inverse coupling `β`. -/
noncomputable def loopCorrelation (k L : ℕ) (β : ℝ) (A : List (Loop d)) : ℂ :=
  expectation (R := L * 2 ^ k) ρ β fun U => loopProduct ρ U k A

end Observables

/-! ### Axioms for the continuum theory -/

section Continuum

variable {d : ℕ}

/-- A family of loops is admissible when each loop is simple and the loops are pairwise
disjoint; the continuum theory is only asked to assign correlation functions to such families. -/
def IsAdmissible (A : List (Loop d)) : Prop :=
  (∀ γ ∈ A, γ.IsSimple) ∧ A.Pairwise Loop.Disjoint

variable {N : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (ρ : G →* Matrix.unitaryGroup (Fin N) ℂ)

/-- `W` is a continuum limit of the Wilson lattice gauge theories with gauge group `(G, ρ)`:
along the lattice spacings `2^{-k}`, with inverse couplings `β k`, boxes of half-side `L k → ∞`,
and positive multiplicative renormalization constants `Z k γ` for each loop, the renormalized
correlation functions of every admissible family of loops converge to `W`. -/
structure IsContinuumLimit (β : ℕ → ℝ) (L : ℕ → ℕ) (Z : ℕ → Loop d → ℝ)
    (W : List (Loop d) → ℂ) : Prop where
  β_pos : ∀ k, 0 < β k
  Z_pos : ∀ k γ, 0 < Z k γ
  L_tendsto : Tendsto L atTop atTop
  tendsto : ∀ A : List (Loop d), IsAdmissible A →
    Tendsto (fun k => ((A.map (Z k)).prod : ℂ) * loopCorrelation ρ k (L k) (β k) A)
      atTop (𝓝 (W A))

/-- Invariance of `W` under the symmetries of the lattice that survive in the continuum:
all dyadic translations and all signed coordinate permutations. -/
structure IsLatticeInvariant (W : List (Loop d) → ℂ) : Prop where
  translate : ∀ (A : List (Loop d)) (j : ℕ) (v : Site d), IsAdmissible A →
    W (A.map fun γ => γ.translate j v) = W A
  mapCoords : ∀ (A : List (Loop d)) (σ : Equiv.Perm (Fin d)) (ε : Fin d → Bool), IsAdmissible A →
    W (A.map fun γ => γ.mapCoords σ ε) = W A

variable [NeZero d]

/-- Osterwalder–Schrader reflection positivity of `W`: for all coefficients `c_i ∈ ℂ` and
admissible families `A_i` of loops with strictly positive time coordinates,
`∑_{i,j} conj(c_i) c_j W(θA_i ∪ A_j)` is real and `≥ 0`, where `θ` is `Loop.reflect`. -/
def IsReflectionPositive (W : List (Loop d) → ℂ) : Prop :=
  ∀ (n : ℕ) (c : Fin n → ℂ) (A : Fin n → List (Loop d)),
    (∀ i, IsAdmissible (A i) ∧ ∀ γ ∈ A i, γ.StrictlyPositiveTime) →
    (∑ i, ∑ j, (starRingEnd ℂ) (c i) * c j * W ((A i).map Loop.reflect ++ A j)).im = 0 ∧
      0 ≤ (∑ i, ∑ j, (starRingEnd ℂ) (c i) * c j * W ((A i).map Loop.reflect ++ A j)).re

/-- `W` has a mass gap of size at least `Δ`: connected correlations between any two admissible
families of loops decay at least like `e^{-Δ t}` in their Euclidean time separation `t`,
`|W(A ∪ τ_t B) - W(A) W(B)| ≤ C_{A,B} e^{-Δ t}` for all dyadic `t = n / 2^j ≥ 0` for which
`A ∪ τ_t B` is admissible.  Under Osterwalder–Schrader reconstruction this is equivalent to the
Hamiltonian having no spectrum in `(0, Δ)`. -/
def HasMassGap (W : List (Loop d) → ℂ) (Δ : ℝ) : Prop :=
  ∀ A B : List (Loop d), IsAdmissible A → IsAdmissible B → ∃ C : ℝ, ∀ j n : ℕ,
    IsAdmissible (A ++ B.map fun γ => γ.timeTranslate j n) →
    ‖W (A ++ B.map fun γ => γ.timeTranslate j n) - W A * W B‖ ≤
      C * Real.exp (-Δ * ((n : ℝ) / 2 ^ j))

/-- Jaffe–Witten's requirement that the mass `m = sup {Δ : W has mass gap Δ}` be finite:
equivalently the theory is not trivial (its Hamiltonian is not zero). -/
def HasFiniteMass (W : List (Loop d) → ℂ) : Prop := ¬ ∀ Δ : ℝ, HasMassGap W Δ

end Continuum

end

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 'The Problem' (definition of the mass gap: 'A quantum field theory has a mass gap Δ if H has no spectrum in the interval (0, Δ) for some Δ > 0. The supremum of such Δ is the mass m, and we require m < ∞'; statement of the problem); p. 11, §6.5 'Yang–Mills Theory' (Wilson's lattice approximation with compact gauge group: 'One must then verify the existence of limits of appropriate expectations of gauge-invariant observables as the lattice spacing tends to zero and as the volume tends to infinity'; reflection positivity of the Wilson approximation). Lattice theory as in K. Osterwalder, E. Seiler, Gauge field theories on a lattice, Ann. Physics 110 (1978), 440–471, https://doi.org/10.1016/0003-4916(78)90039-8 and S. Chatterjee, Yang–Mills for probabilists, Springer Proc. Math. Stat. 283 (2019), §3–§5, https://doi.org/10.1007/978-3-030-15338-0_1

Read-back

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

Read-back: `Def_YangMills` bundle (namespace `YangMills`)

All declarations below live in the namespace YangMills, are noncomputable where marked, and open the Mathlib namespaces for measure theory, filters and topology. Throughout, $d, R, N, k, j, n, T, L \in \mathbb{N} = \{0,1,2,\dots\}$ unless stated otherwise; $\mathbb{N}$ includes $0$ . Subtraction of natural numbers is truncated ( $a - b = 0$ whenever $a \le b$ ); I flag every place it occurs.

`IsCompactSimpleGaugeGroup`

A predicate (a Prop-valued structure) on a type $G$ equipped with only a group structure and a topology. No compatibility between the group law and the topology is assumed (no continuity of multiplication or inversion), no compactness, no Hausdorff-ness, no measurability. The predicate holds iff all three of the following hold:

connected: $G$ is a connected space, i.e. $G$ is nonempty and its underlying set is preconnected (cannot be split by two disjoint nonempty open sets).
nonabelian: there exist $a, b \in G$ with $ab \ne ba$ .
normal_finite_or_top: for every subgroup $K \le G$ which is normal and whose underlying set is closed in the topology of $G$ , either the underlying set of $K$ is finite, or $K = G$ (the top subgroup).

Nothing else is asserted; in particular the name's word "compact" does not correspond to any field.

`Site d`

An abbreviation: a site in dimension $d$ is a function $x : \{0,\dots,d-1\} \to \mathbb{Z}$ , i.e. an element of $\mathbb{Z}^d$ , written $x = (x_0,\dots,x_{d-1})$ . For $d = 0$ there is exactly one site (the empty function). Sites form an additive group under coordinatewise addition, and admit scalar multiplication by integers, $m \cdot x = (m x_\mu)_\mu$ .

`unit d μ`

For $\mu \in \{0,\dots,d-1\}$ , the site $e_\mu \in \mathbb{Z}^d$ with $(e_\mu)_\nu = 1$ if $\nu = \mu$ and $0$ otherwise (the standard basis vector).

`box d R`

The finite set

\Lambda_R := \{\, x \in \mathbb{Z}^d : -R \le x_\mu \le R \text{ for every } \mu \in \{0,\dots,d-1\} \,\},

i.e. the discrete cube $\{-R,\dots,R\}^d$ , constructed as the finite set of functions whose $\mu$ -th value lies in the integer interval $[-R, R]$ for every $\mu$ . It has $(2R+1)^d$ elements; for $d = 0$ it is a singleton, for $R = 0$ it is $\{0\}$ .

`Edge d`

An abbreviation: an edge is a pair $(x, \mu)$ with $x \in \mathbb{Z}^d$ a site and $\mu \in \{0,\dots,d-1\}$ a direction index. No geometric meaning is attached by the type itself.

`boxEdges d R`

The finite set of edges

E_R := \{\, (x,\mu) : x \in \Lambda_R,\ \mu \in \{0,\dots,d-1\},\ x + e_\mu \in \Lambda_R \,\},

obtained by filtering the product of $\Lambda_R$ with the full set of direction indices by the condition that $x + e_\mu$ (the site whose $\mu$ -th coordinate is increased by $1$ ) also lies in $\Lambda_R$ ; equivalently $x_\mu \le R - 1$ . For $d = 0$ this set is empty.

`Plaquette d`

An abbreviation: a plaquette is a triple $(x, \mu, \nu)$ with $x \in \mathbb{Z}^d$ and $\mu, \nu \in \{0,\dots,d-1\}$ , stored as a pair $(x, (\mu,\nu))$ .

`boxPlaquettes d R`

The finite set of plaquettes

P_R := \{\, (x,\mu,\nu) : x \in \Lambda_R,\ \mu < \nu,\ x + e_\mu \in \Lambda_R,\ x + e_\nu \in \Lambda_R,\ x + e_\mu + e_\nu \in \Lambda_R \,\},

obtained by filtering the product $\Lambda_R \times (\text{all } \mu) \times (\text{all } \nu)$ by the conjunction of the four conditions shown. The comparison $\mu < \nu$ is the usual order on $\{0,\dots,d-1\}$ , so each unordered pair of distinct directions appears once. For $d \le 1$ this set is empty.

`Config d R G`

An abbreviation: a configuration is a function $U : E_R \to G$ from the finite set of box edges (as a subtype: an edge together with a proof that it belongs to $E_R$ ) into a type $G$ . In this abbreviation no structure on $G$ is required.

Section `Lattice` (assumptions: $d, R \in \mathbb{N}$ implicit; $G$ a type with a group structure)

`link U e`

For a configuration $U : E_R \to G$ and an arbitrary edge $e = (x,\mu)$ (not necessarily in the box), the group element

\operatorname{link}_U(e) := \begin{cases} U(e) & \text{if } e \in E_R, \\ 1 & \text{otherwise.}\end{cases}

The default value $1$ (identity of $G$ ) is a junk value for edges outside the box.

`plaquette U p`

For a configuration $U$ and an arbitrary plaquette $p = (x, \mu, \nu)$ (no membership in $P_R$ and no $\mu \ne \nu$ required), the group element

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

with products read left to right in the (possibly noncommutative) group $G$ . Links outside $E_R$ contribute $1$ via the default in link.

`gaugeTransform g U`

For a function $g : \mathbb{Z}^d \to G$ (defined on all sites) and a configuration $U$ , the configuration $g \cdot U : E_R \to G$ given on an edge $e = (x,\mu) \in E_R$ by

(g\cdot U)(x,\mu) := g(x)\, U(x,\mu)\, g(x+e_\mu)^{-1}.

`wilsonAction ρ U`

Additional assumptions: $N \in \mathbb{N}$ implicit, and $\rho : G \to \mathrm{U}(N)$ a monoid homomorphism (preserving multiplication and the identity) into the unitary group of $N\times N$ complex matrices $\{A \in M_N(\mathbb{C}) : A^* A = A A^* = I\}$ . No continuity or measurability of $\rho$ is assumed. The Wilson action is the real number

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

where $\rho(\cdot)$ is viewed as an $N\times N$ complex matrix and $\operatorname{tr}$ is the matrix trace. There is no sign, no normalisation constant, and no subtraction of $N$ . If $P_R = \emptyset$ (e.g. $d \le 1$ ) then $S_\rho(U) = 0$ ; if $N = 0$ the trace is $0$ and $S_\rho(U) = 0$ .

Section `Measure` (assumptions: $d,R$ implicit; $G$ a group with a topology making multiplication and inversion continuous, $G$ compact, equipped with a $\sigma$ -algebra which is the Borel $\sigma$ -algebra of the topology)

`haarProb G`

The measure $\mu_G$ on $G$ defined as Mathlib's left Haar measure associated to the positive compact set $\top = G$ (the whole space, which is compact and nonempty since $G$ contains $1$ ). By Mathlib's normalisation this is the left-invariant Haar measure scaled so that $\mu_G(G) = 1$ , i.e. a probability measure. (All typeclass assumptions listed for the section are required explicitly by this definition.)

`configMeasure d R G`

The product measure

\mu_{d,R,G} := \bigotimes_{e \in E_R} \mu_G

on the configuration space $E_R \to G$ : Mathlib's finite product (Measure.pi) of one copy of $\mu_G$ per box edge. When $E_R = \emptyset$ the configuration space is a singleton and this is the Dirac mass of total measure $1$ .

`gibbsWeight ρ β U`

For $\rho : G \to \mathrm{U}(N)$ a monoid homomorphism, $\beta \in \mathbb{R}$ (any sign) and a configuration $U$ , the positive real number

w_{\rho,\beta}(U) := \exp\big(\beta \cdot S_\rho(U)\big),

with $S_\rho$ the Wilson action above (note the sign: $+\beta S$ , not $-\beta S$ ).

`expectation ρ β F`

For $\beta \in \mathbb{R}$ and $F : (E_R \to G) \to \mathbb{C}$ , the complex number

\langle F\rangle_{\rho,\beta} := \frac{\displaystyle\int F(U)\, w_{\rho,\beta}(U)\, d\mu_{d,R,G}(U)}{\displaystyle\int w_{\rho,\beta}(U)\, d\mu_{d,R,G}(U)},

where $w_{\rho,\beta}(U)$ is cast from $\mathbb{R}$ to $\mathbb{C}$ , both integrals are Bochner integrals in $\mathbb{C}$ , and $/$ is division in $\mathbb{C}$ . Junk conventions apply: a Bochner integral of a non-integrable (in particular non-measurable) integrand equals $0$ , and division by $0$ in $\mathbb{C}$ yields $0$ . Since $\rho$ is not assumed continuous or measurable, neither integrand is asserted to be integrable; if the denominator's integral is $0$ (for whatever reason) the expectation is $0$ .

`plaquetteMeasure ρ β`

For $\beta \in \mathbb{R}$ , a measure on $G$ defined as

\nu_{\rho,\beta} := \Big(\operatorname{ofReal}\!\int_G \exp\big(\beta\,\operatorname{Re}\operatorname{tr}\rho(g)\big)\, d\mu_G(g)\Big)^{-1}\cdot \Big(\mu_G \text{ with density } g \mapsto \operatorname{ofReal}\exp\big(\beta\,\operatorname{Re}\operatorname{tr}\rho(g)\big)\Big),

where $\operatorname{ofReal} : \mathbb{R} \to [0,\infty]$ sends negative reals to $0$ , the inner integral is a real Bochner integral (equal to $0$ if the integrand is not integrable), the inverse is taken in $[0,\infty]$ (so $0^{-1} = \infty$ and $\infty^{-1} = 0$ ), "with density" is Mathlib's withDensity (defined for any function via the lower Lebesgue integral, no measurability required), and $\cdot$ is scaling of a measure by an element of $[0,\infty]$ . If the normalising integral evaluates to $0$ the prefactor is $\infty$ .

`Step d`

An abbreviation: a step is a pair $s = (\mu, b)$ with $\mu \in \{0,\dots,d-1\}$ a direction and $b \in \{\mathtt{true},\mathtt{false}\}$ a Boolean.

`stepVec s`

For a step $s = (\mu, b)$ , the site

\vec s := \begin{cases} e_\mu & b = \mathtt{true}, \\ -e_\mu & b = \mathtt{false}.\end{cases}

Section `Paths` ( $d$ implicit)

`pathVertices x [s_1,\dots,s_n]`

Defined recursively on the step list. For a starting site $x$ and steps $s_1,\dots,s_n$ :

\operatorname{pathVertices}(x, [\,]) = [\,], \qquad \operatorname{pathVertices}(x, s :: \text{rest}) = x :: \operatorname{pathVertices}(x + \vec s, \text{rest}),

so the result is the list of $n$ sites $[x,\ x+\vec s_1,\ x+\vec s_1+\vec s_2,\ \dots,\ x+\vec s_1+\dots+\vec s_{n-1}]$ : the starting point of each step, not including the final endpoint $x + \sum_i \vec s_i$ . For the empty step list it is the empty list (the start $x$ is not listed).

`pathEdges x [s_1,\dots,s_n]`

Defined recursively. $\operatorname{pathEdges}(x,[\,]) = [\,]$ , and for a first step $s = (\mu, b)$ ,

\operatorname{pathEdges}(x, s :: \text{rest}) = \Big(\begin{cases}(x, \mu) & b = \mathtt{true} \\ (x - e_\mu, \mu) & b = \mathtt{false}\end{cases}\Big) :: \operatorname{pathEdges}(x + \vec s, \text{rest}).

That is, each step is recorded as the edge $(y,\mu)$ whose lower endpoint $y$ is $x$ for a forward step and $x - e_\mu$ for a backward step, without recording orientation.

`pathHol U x [s_1,\dots,s_n]`

Additional assumptions: $R$ implicit, $G$ a group, $U : E_R \to G$ a configuration. Defined recursively: $\operatorname{hol}_U(x, [\,]) = 1$ , and for a first step $s = (\mu,b)$ ,

\operatorname{hol}_U(x, s :: \text{rest}) = \Big(\begin{cases}\operatorname{link}_U(x,\mu) & b = \mathtt{true} \\ \operatorname{link}_U(x - e_\mu, \mu)^{-1} & b = \mathtt{false}\end{cases}\Big)\cdot \operatorname{hol}_U(x + \vec s, \text{rest}),

i.e. the ordered left-to-right product along the path of the link variables, inverted on backward steps, using $\operatorname{link}_U$ (so any edge outside $E_R$ contributes $1$ ).

`Loop d`

A structure with four fields:

scale $: \mathbb{N}$ , a natural number $k_\gamma$ ;
base $: \mathbb{Z}^d$ , a site $x_\gamma$ ;
steps $:$ a finite list of steps $[s_1,\dots,s_n]$ ;
closed $:$ a proof that $\sum_{i=1}^n \vec s_i = 0$ in $\mathbb{Z}^d$ .

Nothing requires the step list to be nonempty (the empty list is closed), nothing relates scale to base or steps, and no bound on base is imposed. Two loops are equal iff their scale, base and steps agree (the proof field is irrelevant).

Namespace `Loop` ( $d$ implicit throughout)

Auxiliary `sum_map_stepVec_flatMap_replicate n l`

(Proof-obligation lemma.) For every $n$ and step list $l$ , replacing every step of $l$ by $n$ consecutive copies of itself and summing the step vectors gives $n \cdot \sum_{s \in l} \vec s$ .

`refine γ j`

For a loop $\gamma = (k_\gamma, x_\gamma, [s_1,\dots,s_n])$ and $j \in \mathbb{N}$ , the loop

\gamma^{(j)} := \big(\ k_\gamma + j,\quad 2^j\cdot x_\gamma,\quad [\underbrace{s_1,\dots,s_1}_{2^j},\ \underbrace{s_2,\dots,s_2}_{2^j},\ \dots,\ \underbrace{s_n,\dots,s_n}_{2^j}]\ \big),

where $2^j \cdot x_\gamma$ is coordinatewise integer scaling. Its closed field asserts $\sum \vec s = 2^j \cdot \sum_i \vec s_i = 0$ , discharged from $\gamma$ 's closedness via the lemma above. For $j = 0$ , $\gamma^{(0)} = \gamma$ .

`atScale γ k`

For a loop $\gamma$ and $k \in \mathbb{N}$ , the pair (base, steps) of $\gamma^{(k \mathbin{\dot-} k_\gamma)}$ , where $k \mathbin{\dot-} k_\gamma$ is truncated natural subtraction. Explicitly:

\operatorname{atScale}(\gamma, k) = \begin{cases}\big(2^{k - k_\gamma} x_\gamma,\ \text{steps of } \gamma \text{ each repeated } 2^{k-k_\gamma} \text{ times}\big) & k \ge k_\gamma, \\ (x_\gamma,\ \text{steps of } \gamma) & k < k_\gamma \ (\text{no change}).\end{cases}

The scale field of the result is discarded.

`vertices γ`

The list $\operatorname{pathVertices}(x_\gamma, \text{steps}_\gamma)$ : the starting sites of each step of $\gamma$ at its own base and step list (endpoint not repeated; empty if there are no steps).

`verticesAt γ k`

The list $\operatorname{pathVertices}$ applied to the base and steps of $\operatorname{atScale}(\gamma,k)$ , with the truncated-subtraction behaviour above (for $k < k_\gamma$ it equals vertices γ).

`edges γ`

The list $\operatorname{pathEdges}(x_\gamma, \text{steps}_\gamma)$ of (unoriented, lower-endpoint) edges traversed by $\gamma$ at its own base and steps.

`IsSimple γ`

The conjunction of three conditions: the step list of $\gamma$ is nonempty; the list vertices γ has no repeated entries; the list edges γ has no repeated entries. (Both no-repetition conditions are checked as lists at the loop's native scale.)

`Disjoint γ₁ γ₂`

Let $m := \max(k_{\gamma_1}, k_{\gamma_2})$ . The predicate asserts that the lists $\operatorname{verticesAt}(\gamma_1, m)$ and $\operatorname{verticesAt}(\gamma_2, m)$ have no common element: for every site $x$ , it is not the case that $x$ belongs to both lists. (Since $m \ge k_{\gamma_i}$ for both, no truncation occurs here.)

`InBox γ k R`

Every site in the list $\operatorname{verticesAt}(\gamma, k)$ lies in the cube $\Lambda_R = \{-R,\dots,R\}^d$ . Vacuously true if the list is empty (e.g. no steps). Subject to the truncation in atScale when $k < k_\gamma$ .

`translate γ j v`

For a loop $\gamma$ , $j \in \mathbb{N}$ , and a site $v \in \mathbb{Z}^d$ , let $m := \max(k_\gamma, j)$ . The loop with

scale $= m$ ;
base $= 2^{\,m - k_\gamma}\cdot x_\gamma + 2^{\,m - j}\cdot v$ (both exponents are honest since $m \ge k_\gamma$ and $m \ge j$ ; exactly one of them is $0$ unless $k_\gamma = j$ );
steps $=$ the steps of $\gamma$ each repeated $2^{m-k_\gamma}$ times (the steps of $\gamma^{(m-k_\gamma)}$ );
closed $=$ the closedness proof of $\gamma^{(m - k_\gamma)}$ .

Section `Time` (additional assumption: $d \ne 0$ , so that the index $0 \in \{0,\dots,d-1\}$ exists)

`timeTranslate γ j n`

$\operatorname{translate}(\gamma, j, n\cdot e_0)$ : the translate above with $v = (n, 0, \dots, 0)$ , $n \in \mathbb{N}$ cast to $\mathbb{Z}$ .

`PositiveTime γ`

Every site $x$ in the list vertices γ (native scale) satisfies $x_0 \ge 0$ . Vacuous if the list is empty.

`StrictlyPositiveTime γ`

Every site $x$ in the list vertices γ satisfies $x_0 > 0$ . Vacuous if the list is empty.

`timeFlip x`

The site $\theta(x)$ with $\theta(x)_0 = -x_0$ and $\theta(x)_\mu = x_\mu$ for $\mu \ne 0$ .

Auxiliary `timeFlip_add`, `timeFlip_zero`

$\theta(x + y) = \theta(x) + \theta(y)$ and $\theta(0) = 0$ .

`timeFlipHom`

$\theta$ packaged as an additive group homomorphism $\mathbb{Z}^d \to \mathbb{Z}^d$ with the two lemmas above as its axioms.

`reflectStep s`

For $s = (\mu, b)$ :

\operatorname{reflectStep}(\mu, b) := \begin{cases} (\mu, b) & \mu = 0, \\ (\mu, \lnot b) & \mu \ne 0.\end{cases}

That is, steps in direction $0$ are unchanged and steps in every other direction have their Boolean flipped.

Auxiliary `stepVec_reflectStep`, `sum_map_stepVec_reflect`

$\overrightarrow{\operatorname{reflectStep}(s)} = -\theta(\vec s)$ ; and for any step list $l$ , the sum of step vectors of the reversed list of reflected steps equals $-\theta\big(\sum_{s\in l}\vec s\big)$ .

`reflect γ`

The loop with scale $= k_\gamma$ , base $= \theta(x_\gamma)$ , and steps $=$ the list obtained by applying reflectStep to every step of $\gamma$ and then reversing the list. Its closed field asserts the step vectors of this new list sum to $0$ , discharged via the lemma above from $\gamma$ 's closedness.

Section `Hyperoctahedral`

`coordMap σ ε x`

For a permutation $\sigma$ of $\{0,\dots,d-1\}$ , a sign pattern $\varepsilon : \{0,\dots,d-1\} \to \{\mathtt{true},\mathtt{false}\}$ , and a site $x$ , the site

\Phi_{\sigma,\varepsilon}(x)_\mu := \begin{cases} +\,x_{\sigma^{-1}(\mu)} & \varepsilon(\mu) = \mathtt{true} \\ -\,x_{\sigma^{-1}(\mu)} & \varepsilon(\mu) = \mathtt{false}.\end{cases}

Auxiliary `coordMap_add`, `coordMap_zero`

$\Phi_{\sigma,\varepsilon}(x+y) = \Phi_{\sigma,\varepsilon}(x) + \Phi_{\sigma,\varepsilon}(y)$ and $\Phi_{\sigma,\varepsilon}(0) = 0$ .

`coordMapHom σ ε`

$\Phi_{\sigma,\varepsilon}$ packaged as an additive group homomorphism $\mathbb{Z}^d \to \mathbb{Z}^d$ .

`mapStep σ ε s`

For $s = (\mu, b)$ , the step

\operatorname{mapStep}_{\sigma,\varepsilon}(\mu, b) := \big(\sigma(\mu),\ [\,b = \varepsilon(\sigma(\mu))\,]\big),

where the second component is the Boolean " $b$ equals $\varepsilon(\sigma(\mu))$ ": it is $b$ itself when $\varepsilon(\sigma(\mu)) = \mathtt{true}$ and $\lnot b$ when $\varepsilon(\sigma(\mu)) = \mathtt{false}$ .

Auxiliary `stepVec_mapStep`

$\overrightarrow{\operatorname{mapStep}_{\sigma,\varepsilon}(s)} = \Phi_{\sigma,\varepsilon}(\vec s)$ .

`mapCoords γ σ ε`

The loop with scale $= k_\gamma$ , base $= \Phi_{\sigma,\varepsilon}(x_\gamma)$ , steps $=$ the list of $\operatorname{mapStep}_{\sigma,\varepsilon}(s_i)$ in the original order. Its closed field asserts the new step vectors sum to $0$ , discharged from $\gamma$ 's closedness using additivity of $\Phi_{\sigma,\varepsilon}$ .

`rect k T R μ ν`

For $k, T, R \in \mathbb{N}$ and directions $\mu, \nu \in \{0,\dots,d-1\}$ (not required to be distinct), the loop with scale $= k$ , base $= 0$ , and steps equal to the concatenation

[\underbrace{(\mu,\mathtt{true}),\dots}_{T}] \mathbin{+\!\!+} [\underbrace{(\nu,\mathtt{true}),\dots}_{R}] \mathbin{+\!\!+} [\underbrace{(\mu,\mathtt{false}),\dots}_{T}] \mathbin{+\!\!+} [\underbrace{(\nu,\mathtt{false}),\dots}_{R}],

i.e. $T$ forward steps in direction $\mu$ , $R$ forward in $\nu$ , $T$ backward in $\mu$ , $R$ backward in $\nu$ . Its closed field asserts $T e_\mu + R e_\nu - T e_\mu - R e_\nu = 0$ . If $T = R = 0$ the step list is empty; if $\mu = \nu$ the path retraces itself. (Here $R$ is a parameter of rect, unrelated to a box radius.)

Section `Observables` (assumptions: $d, R, N$ implicit; $G$ a group; $\rho : G \to \mathrm{U}(N)$ a monoid homomorphism)

`wilsonLoop ρ U k γ`

For a configuration $U : E_R \to G$ , a scale $k \in \mathbb{N}$ , and a loop $\gamma$ , the complex number

W_\rho(U, k, \gamma) := \operatorname{tr}\, \rho\big(\operatorname{hol}_U(\operatorname{atScale}(\gamma,k))\big),

i.e. the trace of the $N \times N$ matrix $\rho$ applied to the path holonomy of $U$ along the base and step list of $\operatorname{atScale}(\gamma, k)$ (with the truncation convention: for $k < k_\gamma$ the loop's own base and steps are used). Links outside $E_R$ contribute $1$ . For an empty step list the holonomy is $1$ and the value is $\operatorname{tr} I_N = N$ .

`loopProduct ρ U k A`

For a list of loops $A = [\gamma_1,\dots,\gamma_m]$ , the complex product $\prod_{i=1}^m W_\rho(U,k,\gamma_i)$ (in list order; equals $1$ for the empty list).

`loopCorrelation ρ k L β A`

Additional assumptions: $G$ is a topological group, compact, with its Borel $\sigma$ -algebra. For $k, L \in \mathbb{N}$ , $\beta \in \mathbb{R}$ , and a list of loops $A$ , the complex number

\big\langle\, U \mapsto \textstyle\prod_{\gamma \in A} W_\rho(U,k,\gamma) \,\big\rangle_{\rho,\beta}

computed by expectation on the configuration space of box radius $R := L \cdot 2^k$ , i.e. over $E_{L 2^k} \to G$ with measure $\bigotimes_{e\in E_{L2^k}} \mu_G$ , with all the junk conventions of expectation (non-integrable integrands give $0$ ; division by $0$ gives $0$ ). When $L = 0$ the box is $\{0\}$ and $E_0 = \emptyset$ .

Section `Continuum` ( $d$ implicit)

`IsAdmissible A`

For a list of loops $A = [\gamma_1,\dots,\gamma_m]$ : every $\gamma_i$ satisfies IsSimple (nonempty steps, no repeated vertex, no repeated edge at native scale), and the list is pairwise Disjoint in the sense that for every pair of positions $i < j$ , $\operatorname{Disjoint}(\gamma_i, \gamma_j)$ holds (vertex lists at the common scale $\max(k_{\gamma_i},k_{\gamma_j})$ share no site). The empty list is admissible.

`IsContinuumLimit ρ β L Z W`

Assumptions: $N$ implicit; $G$ a compact topological group with Borel $\sigma$ -algebra; $\rho : G \to \mathrm{U}(N)$ a monoid homomorphism (no continuity assumed). Data: $\beta : \mathbb{N} \to \mathbb{R}$ , $L : \mathbb{N} \to \mathbb{N}$ , $Z : \mathbb{N} \to \operatorname{Loop}_d \to \mathbb{R}$ , $W : \operatorname{List}(\operatorname{Loop}_d) \to \mathbb{C}$ . The predicate holds iff all of:

β_pos: $\beta_k > 0$ for every $k$ .
Z_pos: $Z_k(\gamma) > 0$ for every $k$ and every loop $\gamma$ .
L_tendsto: $L_k \to \infty$ as $k \to \infty$ (for every $M$ , eventually $L_k \ge M$ ).
tendsto: for every admissible list $A$ ,

\lim_{k\to\infty}\ \Big(\prod_{\gamma \in A} Z_k(\gamma)\Big)\cdot \operatorname{loopCorrelation}(\rho, k, L_k, \beta_k, A) \;=\; W(A)

in $\mathbb{C}$ (the real product is cast to $\mathbb{C}$ ; convergence is with respect to the standard topology on $\mathbb{C}$ , along $k \to \infty$ in $\mathbb{N}$ ).

No condition is placed on $W$ for non-admissible lists, and no condition relates $Z$ to anything else.

`IsLatticeInvariant W`

For $W : \operatorname{List}(\operatorname{Loop}_d) \to \mathbb{C}$ , both of:

translate: for every list $A$ , every $j \in \mathbb{N}$ , every site $v$ , if $A$ is admissible then $W\big([\operatorname{translate}(\gamma, j, v) : \gamma \in A]\big) = W(A)$ .
mapCoords: for every list $A$ , every permutation $\sigma$ of $\{0,\dots,d-1\}$ , every $\varepsilon : \{0,\dots,d-1\}\to\{\mathtt{true},\mathtt{false}\}$ , if $A$ is admissible then $W\big([\operatorname{mapCoords}(\gamma,\sigma,\varepsilon) : \gamma \in A]\big) = W(A)$ .

Only the source list is required to be admissible; nothing is required of the transformed list.

`IsReflectionPositive W`

Assumption: $d \ne 0$ . For $W : \operatorname{List}(\operatorname{Loop}_d) \to \mathbb{C}$ : for every $n \in \mathbb{N}$ , every family of coefficients $c : \{0,\dots,n-1\} \to \mathbb{C}$ , and every family of loop lists $A : \{0,\dots,n-1\} \to \operatorname{List}(\operatorname{Loop}_d)$ , if for every $i$ the list $A_i$ is admissible and every loop in $A_i$ satisfies StrictlyPositiveTime (all its native-scale vertices have $x_0 > 0$ ), then the complex number

Q := \sum_{i=0}^{n-1}\sum_{j=0}^{n-1} \overline{c_i}\, c_j\, W\big(\operatorname{reflect}(A_i) \mathbin{+\!\!+} A_j\big),

where $\operatorname{reflect}(A_i)$ is the list obtained by applying Loop.reflect to each loop of $A_i$ and $\mathbin{+\!\!+}$ is list concatenation, satisfies $\operatorname{Im} Q = 0$ and $\operatorname{Re} Q \ge 0$ . For $n = 0$ the sums are empty and the conclusion holds trivially.

`HasMassGap W Δ`

Assumption: $d \ne 0$ . For $W : \operatorname{List}(\operatorname{Loop}_d) \to \mathbb{C}$ and $\Delta \in \mathbb{R}$ (any sign): for every two admissible lists $A, B$ there exists a real constant $C$ (any sign allowed, depending on $A, B$ ) such that for every $j, n \in \mathbb{N}$ , if the concatenated list $A \mathbin{+\!\!+} [\operatorname{timeTranslate}(\gamma, j, n) : \gamma \in B]$ is admissible, then

\Big\| W\big(A \mathbin{+\!\!+} [\operatorname{timeTranslate}(\gamma,j,n) : \gamma\in B]\big) - W(A)\, W(B) \Big\| \;\le\; C \cdot \exp\!\Big(-\Delta \cdot \frac{n}{2^{j}}\Big),

where $\|\cdot\|$ is the modulus on $\mathbb{C}$ , $n$ is cast to $\mathbb{R}$ and $n / 2^j$ is real division. For pairs $(j,n)$ for which the concatenated list is not admissible, nothing is asserted; if no such pair exists the condition on $C$ is vacuous.

`HasFiniteMass W`

Assumption: $d \ne 0$ . The negation of "for every $\Delta \in \mathbb{R}$ , HasMassGap W Δ"; equivalently, there exists some $\Delta \in \mathbb{R}$ (possibly negative or zero) for which HasMassGap W Δ fails.

View graph

Wilson lattice Yang–Mills theory with compact simple gauge group: gauge fields, Wilson loops, dyadic loops, and the axioms for a continuum theory with a mass gap (Jaffe–Witten §4, §6.5)

Read-back: Def_YangMills bundle (namespace YangMills)

IsCompactSimpleGaugeGroup

Site d

unit d μ

box d R

Edge d

boxEdges d R

Plaquette d

boxPlaquettes d R

Config d R G

Section Lattice (assumptions: d,R∈Nd, R \in \mathbb{N}d,R∈N implicit; GGG a type with a group structure)

link U e

plaquette U p

gaugeTransform g U

wilsonAction ρ U

Section Measure (assumptions: d,Rd,Rd,R implicit; GGG a group with a topology making multiplication and inversion continuous, GGG compact, equipped with a σ\sigmaσ-algebra which is the Borel σ\sigmaσ-algebra of the topology)

haarProb G

configMeasure d R G

gibbsWeight ρ β U

expectation ρ β F

plaquetteMeasure ρ β

Step d

stepVec s

Section Paths (ddd implicit)

pathVertices x [s_1,\dots,s_n]

pathEdges x [s_1,\dots,s_n]

pathHol U x [s_1,\dots,s_n]

Loop d

Namespace Loop (ddd implicit throughout)

Auxiliary sum_map_stepVec_flatMap_replicate n l

refine γ j

atScale γ k

vertices γ

verticesAt γ k

edges γ

IsSimple γ

Disjoint γ₁ γ₂

InBox γ k R

translate γ j v

Section Time (additional assumption: d≠0d \ne 0d=0, so that the index 0∈{0,…,d−1}0 \in \{0,\dots,d-1\}0∈{0,…,d−1} exists)

timeTranslate γ j n

PositiveTime γ

StrictlyPositiveTime γ

timeFlip x

Auxiliary timeFlip_add, timeFlip_zero

timeFlipHom

reflectStep s

Auxiliary stepVec_reflectStep, sum_map_stepVec_reflect

reflect γ

Section Hyperoctahedral

coordMap σ ε x

Auxiliary coordMap_add, coordMap_zero

coordMapHom σ ε

mapStep σ ε s

Auxiliary stepVec_mapStep

mapCoords γ σ ε

rect k T R μ ν

Section Observables (assumptions: d,R,Nd, R, Nd,R,N implicit; GGG a group; ρ:G→U(N)\rho : G \to \mathrm{U}(N)ρ:G→U(N) a monoid homomorphism)

wilsonLoop ρ U k γ

loopProduct ρ U k A

loopCorrelation ρ k L β A

Section Continuum (ddd implicit)

IsAdmissible A

IsContinuumLimit ρ β L Z W

IsLatticeInvariant W

IsReflectionPositive W

HasMassGap W Δ

HasFiniteMass W