MassGapCont
plain-language theorem explainer
MassGapCont γ asserts existence of a lattice measure μ such that the lattice mass gap holds at γ and the gap persists. Researchers working on the continuum limit of lattice Yang-Mills theories cite this definition when packaging stability for Osterwalder-Schrader reconstruction. The definition is a direct existential packaging of the MassGap predicate and the GapPersists hypothesis.
Claim. The continuum mass gap predicate for real parameter $γ$ is the statement that there exists an abstract lattice measure $μ$ such that the lattice mass gap condition holds at $γ$ and the gap persistence hypothesis $0 < γ$ is satisfied.
background
In the YM.OS module, LatticeMeasure is an abstract structure serving as an interface for lattice measures on which transfer kernels act. MassGap μ γ is defined as the existence of a kernel K such that the transfer operator exhibits a Perron-Frobenius gap of size γ. GapPersists γ is the hypothesis that γ is strictly positive, encoding the stability required for the continuum limit.
proof idea
This is a direct definition that existentially quantifies over lattice measures μ satisfying the conjunction of MassGap μ γ and GapPersists γ. No lemmas or tactics are invoked beyond the body of the existential.
why it matters
MassGapCont is used by the downstream theorem mass_gap_continuum, which constructs the continuum mass gap from lattice data under the persistence hypothesis. It packages the stability step that bridges discrete Yang-Mills spectra to the continuum in the Recognition framework, sitting downstream of gap derivations that fix the gap value at 45 and upstream of full Osterwalder-Schrader reconstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.