sigma_nu_weak_ref_cm2

formal source

  44def gev2_to_cm2 : ℝ := 0.3894e-27
  45
  46/-- Named weak-channel reference cross-section in cm^2. -/
  47def sigma_nu_weak_ref_cm2 : ℝ :=
  48  row_fermi_pred ^ (2 : ℕ) * E_ref_GeV ^ (2 : ℕ) * gev2_to_cm2
  49
  50/-- Derived absolute dark-matter cross-section in cm^2 on this reference. -/
  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 :