`MassGap`

definition

show as: view math explainer →

module: IndisputableMonolith.YM.OS
domain: YM
line: 48 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.YM.OS on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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⟩
  62
  63end
  64end OS
  65end YM
  66end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.