Papers With

← All papers
First page of A gauge-invariant measure for lattice chiral fermions

A gauge-invariant measure for lattice chiral fermions

Nathaniel Craig

hep-lat Oct 6, 2026 · v1 hep-ph hep-th
formalization physics
Read PDF arXiv abstract
TL;DR
The mathematical statements and main proof are formalized in a sixteen-module Lean 4 development, kernel-checked with standard axioms and no sorries, provided as supplementary material.
Abstract
We nonperturbatively construct a gauge-invariant measure for overlap fermions on four-dimensional Euclidean lattices in a class of nonabelian chiral gauge theories that includes the Standard Model. On admissible gauge fields, comparing chiral projectors at successive lattice spacings yields an exponentially local current and establishes the global properties needed for Lüscher's reconstruction of a smooth, gauge-invariant fermion measure. This provides a candidate nonperturbative lattice definition of the Standard Model.
Problem

Nonabelian chiral gauge theories, including the Standard Model, have lacked a nonperturbative lattice definition that respects both gauge invariance and chiral symmetry. For overlap fermions, the remaining obstacle is a smooth, local, gauge-invariant fermion measure meeting Lüscher's reconstruction criteria.

Approach

Admissible gauge fields are used to reconstruct a smooth SU(5) connection, which is then sampled on successively finer auxiliary lattices. Chiral projectors at adjacent spacings are interpolated, and a finite comparison identity gives contributions to the measure term. For R=10⊕5̄, an exact color-trace cancellation makes these contributions summable into an exponentially local current, and gauge covariance and lattice symmetries are proved directly. The mathematical statements are formalized in Lean 4 as a supplement.

Figure 2: Reconstruction and sampling of the gauge links. (a) The original gauge links U , shown schematically in two dimensions. (b) We reconstruct a smooth gauge connection \nabla^{0}[U] locally from these links, represented here by the shading. (c) We use parallel transport of the same connection along shorter edges to obtain (e.g.) the finer link fields F_{1/3}U and F_{1/9}U , with spacings on
Results

The authors construct a gauge-invariant measure for a class of chiral gauge theories that includes all four global forms of the Standard Model gauge group, giving a candidate nonperturbative lattice definition. All sixteen Lean modules compiled without errors or warnings, and the proofs were replayed in Lean's kernel using only standard axioms.