IsInPredictedBand

formal source

  59    nlinarith [h_lo, h_hi]
  60
  61/-- Detection within the predicted band of cross-section is consistent. -/
  62def IsInPredictedBand (sigma_meas : ℝ) (sigma_nu : ℝ) : Prop :=
  63  0.11 * sigma_nu < sigma_meas ∧ sigma_meas < 0.13 * sigma_nu
  64
  65/-- Exclusion below the predicted band of cross-section is a falsifier. -/
  66def FalsifiesPrediction (sigma_excl : ℝ) (sigma_nu : ℝ) : Prop :=
  67  sigma_excl < 0.11 * sigma_nu
  68
  69/-- Predicted band and exclusion-falsifier are mutually exclusive in the
  70following sense: a measurement σ that simultaneously sits in the
  71predicted band and falsifies the prediction is impossible. -/
  72theorem band_excludes_falsifier {sigma sigma_nu : ℝ} :
  73    ¬ (IsInPredictedBand sigma sigma_nu ∧ FalsifiesPrediction sigma sigma_nu) := by
  74  rintro ⟨⟨h_lo, _⟩, h_excl⟩
  75  exact (lt_irrefl _) (lt_trans h_excl h_lo)
  76
  77structure DarkMatterCrossSectionCert where
  78  ratio_pos : 0 < crossSectionRatio
  79  ratio_band : 0.11 < crossSectionRatio ∧ crossSectionRatio < 0.13
  80  band_excludes_falsifier :
  81    ∀ {sigma sigma_nu : ℝ},
  82      ¬ (IsInPredictedBand sigma sigma_nu ∧ FalsifiesPrediction sigma sigma_nu)
  83
  84/-- Dark-matter-cross-section bound certificate. -/
  85def darkMatterCrossSectionCert : DarkMatterCrossSectionCert where
  86  ratio_pos := crossSectionRatio_pos
  87  ratio_band := crossSectionRatio_band
  88  band_excludes_falsifier := band_excludes_falsifier
  89
  90end
  91end DarkMatterCrossSectionBound
  92end Cosmology