OSPositivity

formal source

  28/-- OS reflection positivity surrogate: existence of a transfer kernel with a
  29    uniform overlap lower bound β ∈ (0,1]. This encodes a spectral positivity
  30    guard compatible with Dobrushin-type contraction. -/
  31def OSPositivity (_μ : LatticeMeasure) : Prop := ∃ K : Kernel, ∃ β : ℝ, OverlapLowerBoundOS K β
  32
  33lemma OSPositivity_default (_μ : LatticeMeasure) : OSPositivity _μ := by
  34  refine ⟨default, 1, ?_⟩
  35  dsimp [OverlapLowerBoundOS]
  36  constructor <;> norm_num
  37
  38/-- Overlap lower bound for a kernel (β ∈ (0,1]). -/
  39def OverlapLowerBoundOS (_K : Kernel) (β : ℝ) : Prop := 0 < β ∧ β ≤ 1
  40
  41/-- Perron–Frobenius transfer spectral gap property. -/
  42def TransferPFGap (_μ : LatticeMeasure) (_K : Kernel) (γ : ℝ) : Prop := 0 < γ
  43
  44/-- Gap persistence hypothesis (continuum stability). -/
  45def GapPersists (γ : ℝ) : Prop := 0 < γ
  46
  47/-- Lattice mass gap: existence of a kernel with PF gap γ. -/
  48def MassGap (_μ : LatticeMeasure) (γ : ℝ) : Prop := ∃ K : Kernel, TransferPFGap (μ:=default) K γ
  49
  50/-- Continuum mass gap: lattice gap persists via stability hypothesis. -/
  51def MassGapCont (γ : ℝ) : Prop := ∃ μ : LatticeMeasure, MassGap μ γ ∧ GapPersists γ
  52
  53/-- OS positivity + PF transfer gap yields a lattice mass gap. -/
  54theorem mass_gap_of_OS_PF {μ : LatticeMeasure} {K : Kernel} {γ : ℝ}
  55    (hOS : OSPositivity μ) (hPF : TransferPFGap μ K γ) : MassGap μ γ := by
  56  exact ⟨K, hPF⟩
  57
  58/-- Lattice gap persists to continuum under stability hypothesis. -/
  59theorem mass_gap_continuum {μ : LatticeMeasure} {γ : ℝ}
  60    (hGap : MassGap μ γ) (hPers : GapPersists γ) : MassGapCont γ := by
  61  exact ⟨μ, hGap, hPers⟩