OSPositivity
plain-language theorem explainer
OSPositivity(μ) asserts that a lattice measure admits a transfer kernel K together with some β ∈ (0,1] satisfying the overlap lower bound predicate. Lattice gauge theorists studying reflection positivity would cite this as a Dobrushin-compatible spectral guard in the OS setting. The declaration is a direct existential definition over the kernel and bound structures.
Claim. For a lattice measure $μ$, the property OSPositivity($μ$) holds if there exists a transfer kernel $K$ and a real number $β$ such that $0 < β ≤ 1$.
background
LatticeMeasure is an abstract interface for lattice measures. Kernel is the structure carrying a continuous linear transfer operator $T$ acting on complex observables over the lattice. OverlapLowerBoundOS($K$, $β$) is the predicate $0 < β ∧ β ≤ 1$, which supplies a uniform lower bound on kernel overlap.
proof idea
The declaration is a definition. It directly encodes the existential claim over Kernel and the overlap predicate without reduction steps or tactics.
why it matters
OSPositivity supplies the positivity hypothesis for the theorem mass_gap_of_OS_PF, which concludes that OS positivity plus a Perron-Frobenius transfer gap yields a lattice mass gap. It aligns with the Recognition Science mass-gap formula on the phi-ladder and the eight-tick octave. The sibling lemma OSPositivity_default exhibits the trivial case with the default kernel and β = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.