row_weak_ref_cross_section_band

formal source

  51def sigma_DM_weak_ref_cm2 : ℝ :=
  52  sigma_DM_over_sigma_nu_RS * sigma_nu_weak_ref_cm2
  53
  54theorem row_weak_ref_cross_section_band :
  55    5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38 := by
  56  unfold sigma_nu_weak_ref_cm2 E_ref_GeV gev2_to_cm2
  57  have hgf := row_fermi_pred_bracket
  58  have hgf_pos : 0 < row_fermi_pred := by linarith [hgf.1]
  59  constructor
  60  · nlinarith [hgf.1, hgf_pos]
  61  · nlinarith [hgf.2, hgf_pos]
  62
  63theorem row_sigma_DM_weak_ref_band :
  64    5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39 := by
  65  unfold sigma_DM_weak_ref_cm2
  66  have href := row_weak_ref_cross_section_band
  67  have hratio := row_sigma_ratio_band
  68  have href_pos : 0 < sigma_nu_weak_ref_cm2 := by linarith [href.1]
  69  have hratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by linarith [hratio.1]
  70  constructor
  71  · nlinarith [href.1, hratio.1, href_pos, hratio_pos]
  72  · nlinarith [href.2, hratio.2, href_pos, hratio_pos]
  73
  74structure DarkMatterWeakReferenceCrossSectionScoreCardCert where
  75  weak_ref_band :
  76    5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38
  77  sigma_dm_band :
  78    5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39
  79  fermi_bracket :
  80    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ)
  81  sigma_ratio_band :
  82    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  83
  84theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds :