No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
48def MassGap (_μ : LatticeMeasure) (γ : ℝ) : Prop := ∃ K : Kernel, TransferPFGap (μ:=default) K γ
proof body
Definition body.
49
50/-- Continuum mass gap: lattice gap persists via stability hypothesis. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
default
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
default
in IndisputableMonolith.Config.Flags
decl_use
-
K
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
via
in IndisputableMonolith.Derivations.MassToLight
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
-
TransferPFGap
in IndisputableMonolith.YM.OS
decl_use