mass_gap_of_OS_PF
plain-language theorem explainer
OS positivity on a lattice measure together with a Perron-Frobenius gap on its transfer kernel directly yields the lattice mass gap. Constructive field theorists working on reflection positivity and spectral gaps would cite this when assembling discrete Yang-Mills models. The proof is a one-line term-mode wrapper that packages the supplied kernel and gap hypothesis into the existential witness for MassGap.
Claim. If a lattice measure $μ$ satisfies OS positivity and a transfer kernel $K$ has Perron-Frobenius gap $γ > 0$, then $μ$ admits a mass gap of size $γ$.
background
LatticeMeasure provides an abstract interface for measures on the lattice. Kernel encodes a transfer operator acting as a continuous linear map on complex observables over the lattice. OSPositivity asserts existence of a kernel together with an overlap lower bound $β ∈ (0,1]$, serving as a surrogate for reflection positivity compatible with Dobrushin contraction. TransferPFGap requires only that the gap parameter $γ$ be strictly positive, capturing the Perron-Frobenius spectral gap property. MassGap is the existential statement that some kernel satisfies the positive-gap condition for the given measure.
proof idea
The proof is a term-mode one-liner that applies exact to the pair ⟨K, hPF⟩, directly witnessing the existential quantifier inside the definition of MassGap.
why it matters
This theorem supplies the lattice mass gap from OS positivity and transfer gap assumptions inside the YM.OS development. It forms the discrete foundation for later continuum statements in the Recognition Science treatment of Yang-Mills, consistent with the framework's use of the phi-ladder and forcing chain to derive gaps. No downstream uses are recorded yet, leaving open the question of how the lattice gap lifts under the stability hypotheses appearing in related modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.