def definition def or abbrev

`darkMatterMassCert`

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

formal statement (Lean)

  44noncomputable def darkMatterMassCert : DarkMatterMassCert where
  45  gap45_val := gap45_eq

Definition body.

  46  mass_ratio := dmMassRatio_eq
  47  mDM_band := mDM_band
  48
  49end IndisputableMonolith.Physics.DarkMatterMassFromGap45

Lean names referenced from this declaration's body.

gap45_eq in IndisputableMonolith.CrossDomain.CardinalitySpectrum decl_use
gap45_eq in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
DarkMatterMassCert in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
dmMassRatio_eq in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
gap45_eq in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
mDM_band in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
mass_ratio in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder decl_use
mass_ratio in IndisputableMonolith.Physics.NeutrinoMassFromPhiLadder decl_use
mass_ratio in IndisputableMonolith.StandardModel.PMNSMatrix decl_use