OSPositivity_default
plain-language theorem explainer
The lemma shows that every abstract lattice measure satisfies OS positivity by exhibiting a transfer kernel with uniform overlap lower bound β=1. Researchers modeling lattice Yang-Mills or spectral positivity via recognition kernels would cite this default case. The proof is a direct term construction that instantiates the existential witness with the default kernel and discharges the bound by numerical simplification.
Claim. For every abstract lattice measure $μ$, there exists a transfer kernel $K$ and a real number $β ∈ (0,1]$ such that the overlap lower bound condition holds for $K$ and $β$.
background
LatticeMeasure is an abstract structure for lattice measures that derives Inhabited, guaranteeing a default instance. OSPositivity is the proposition that there exists a Kernel together with $β ∈ (0,1]$ satisfying OverlapLowerBoundOS $K$ $β$; the definition serves as a surrogate for OS reflection positivity and a spectral positivity guard compatible with Dobrushin-type contraction. The lemma sits inside the YM.OS module, which builds concrete transfer operators on top of default configurations.
proof idea
The term proof refines the existential by supplying the default kernel and $β=1$, then applies dsimp on OverlapLowerBoundOS followed by constructor and norm_num to verify the bound holds by direct numerical evaluation.
why it matters
This declaration supplies the canonical default instance of OS positivity inside the YM.OS module, providing the base case for transfer-operator and mass-gap arguments developed in the same file. It instantiates the positivity surrogate required for spectral properties in the recognition framework, consistent with kernel families and self-similar structures. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.