def
definition
MassGapCont
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.YM.OS on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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