GapPersists
plain-language theorem explainer
GapPersists γ asserts that the lattice mass gap parameter remains strictly positive. Researchers deriving continuum limits for Yang-Mills theories in Recognition Science cite it to enforce stability when lifting lattice results. The declaration is a direct abbreviation of the real-number positivity predicate with no lemmas or tactics applied.
Claim. The gap persistence hypothesis holds precisely when the real parameter γ satisfies γ > 0.
background
In the YM.OS module the Osterwalder-Schrader construction equips a LatticeMeasure with a transfer operator whose spectral gap is the real parameter γ. Upstream results include the gap derivation stating that the gap equals 45 as the product of closure and Fibonacci factors, the BIT kernel families supplying exponential and constant kernels, and the J-cost structure from PhiForcingDerived together with spectral emergence of SU(3)×SU(2)×U(1) gauge content. The local setting assumes the mass-gap predicate MassGap μ γ on a lattice measure μ.
proof idea
This is a one-line definition that directly expands to the inequality 0 < γ on the reals. No upstream lemmas are invoked and no tactics are required.
why it matters
GapPersists supplies the stability hypothesis required by the downstream theorem mass_gap_continuum, which concludes that the lattice mass gap persists to the continuum. It bridges the discrete gap of 45 obtained in Gap45.Derivation to the continuum limit while preserving the eight-tick octave and D = 3 spatial dimensions of the Recognition Science forcing chain. The parent result MassGapCont packages the same hypothesis with the lattice mass-gap predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.