OSPositivity_default
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the overlap bound for non-default lattice measures.
- Does not compute explicit eigenvalues or spectral gaps of the kernel.
- Does not address continuum limits or mass-gap persistence.
- Does not invoke the forcing chain or phi-ladder constructions.
formal statement (Lean)
33lemma OSPositivity_default (_μ : LatticeMeasure) : OSPositivity _μ := by
proof body
Term-mode proof.
34 refine ⟨default, 1, ?_⟩
35 dsimp [OverlapLowerBoundOS]
36 constructor <;> norm_num
37
38/-- Overlap lower bound for a kernel (β ∈ (0,1]). -/