theorem proved term proof

`mass_gap_of_OS_PF`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  54theorem mass_gap_of_OS_PF {μ : LatticeMeasure} {K : Kernel} {γ : ℝ}
  55    (hOS : OSPositivity μ) (hPF : TransferPFGap μ K γ) : MassGap μ γ := by

proof body

Term-mode proof.

  56  exact ⟨K, hPF⟩
  57
  58/-- Lattice gap persists to continuum under stability hypothesis. -/

depends on (12)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
Kernel in IndisputableMonolith.ILG.PressureForm decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
Kernel in IndisputableMonolith.YM.OS decl_use
LatticeMeasure in IndisputableMonolith.YM.OS decl_use
MassGap in IndisputableMonolith.YM.OS decl_use
OSPositivity in IndisputableMonolith.YM.OS decl_use
TransferPFGap in IndisputableMonolith.YM.OS decl_use