  49  · nlinarith [h.1]
  50  · nlinarith [h.2]
  51
  52structure DarkMatterAbsoluteCrossSectionScoreCardCert where
  53  sigma_nu_ref_pos : 0 < sigma_nu_reference_cm2
  54  sigma_ratio_band :
  55    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  56  sigma_absolute_band : 1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39
  57
  58theorem darkMatterAbsoluteCrossSectionScoreCardCert_holds :
  59    Nonempty DarkMatterAbsoluteCrossSectionScoreCardCert :=
  60  ⟨{ sigma_nu_ref_pos := row_sigma_nu_reference_pos
  61     sigma_ratio_band := row_sigma_ratio_band
  62     sigma_absolute_band := row_sigma_DM_cm2_band }⟩
  63
  64end
  65
  66end IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard

papers checked against this theorem

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