MassGap
plain-language theorem explainer
MassGap defines the lattice mass gap for a given measure and gap parameter γ as the existence of a transfer kernel satisfying the Perron-Frobenius condition. Constructive QFT researchers cite it when formulating the Yang-Mills mass gap on the lattice before taking the continuum limit. The definition is a direct existential wrapper around the positivity predicate TransferPFGap.
Claim. For a lattice measure $μ$ and real parameter $γ$, the lattice mass gap holds when there exists a transfer kernel $K$ such that the Perron-Frobenius spectral gap condition $0 < γ$ is satisfied.
background
LatticeMeasure supplies an abstract interface for measures on the lattice. Kernel encodes a transfer operator acting on complex-valued observables via a continuous linear map. TransferPFGap is the predicate that simply asserts positivity of the gap parameter γ. This definition sits inside the YM.OS module, which assembles Osterwalder-Schrader positivity, transfer operators, and gap persistence for lattice Yang-Mills.
proof idea
One-line definition that directly packages the existential claim over kernels satisfying the gap predicate.
why it matters
MassGap supplies the core lattice predicate consumed by MassGapCont, mass_gap_continuum, and mass_gap_of_OS_PF. It fills the lattice-level step toward the Recognition Science mass-gap derivation that produces the numerical value 45 from closure and Fibonacci factors. The construction links to the phi-ladder and the eight-tick octave while remaining inside the lattice setting before continuum extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.