mass_gap_continuum
plain-language theorem explainer
The theorem asserts that whenever a lattice measure μ admits a transfer kernel with Perron-Frobenius gap γ and the gap-stability condition holds, the continuum mass gap exists. Workers in constructive quantum field theory cite it when passing from discrete Yang-Mills lattices to their continuum limits. The proof is a direct term that witnesses the existential definition of MassGapCont by packaging the supplied measure and the two hypotheses.
Claim. Let $μ$ be a lattice measure and $γ ∈ ℝ$. If there exists a transfer kernel such that the Perron-Frobenius gap equals $γ$ and $γ > 0$, then there exists a lattice measure satisfying both the lattice gap condition and the persistence hypothesis.
background
In the YM.OS module the structure LatticeMeasure supplies an abstract interface for measures on which transfer operators act. MassGap μ γ is the proposition that some kernel K satisfies TransferPFGap K γ. GapPersists γ is simply the inequality 0 < γ, encoding the stability hypothesis needed for the continuum limit. MassGapCont γ is the existential statement ∃ μ, MassGap μ γ ∧ GapPersists γ.
proof idea
The proof is a one-line term that applies the definition of MassGapCont by supplying the concrete witness μ together with the two input hypotheses.
why it matters
The result supplies the basic persistence step that lifts a lattice mass gap to the continuum under the stability hypothesis. It sits inside the OS-positivity and transfer-operator framework for Yang-Mills theories and completes the elementary implication from lattice gap plus positivity to the continuum statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.