IndisputableMonolith.Cosmology.DarkMatterXENONPrediction

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Dark Matter XENON Prediction — A6 Cosmology Depth
   7
   8From the RS dark matter module: m_DM / m_W = 1/45, predicting
   9m_DM ∈ (1.77, 1.79) GeV.
  10
  11The predicted cross-section band = J(φ) ∈ (0.11, 0.13).
  12XENONnT current exclusion at m_DM = 1.78 GeV is still above the
  13RS prediction.
  14
  15Lean formalisation: prove cross-section ratio in J(φ) band.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Cosmology.DarkMatterXENONPrediction
  21open Constants Cost
  22
  23/-- Predicted DM mass / W mass = 1/45. -/
  24noncomputable def dmMassRatio : ℝ := 1 / 45
  25
  26/-- DM cross-section ratio at J(φ). -/
  27noncomputable def dmCrossSectionRatio : ℝ := Jcost phi
  28
  29/-- Cross-section ratio is positive. -/
  30theorem dmCrossSection_pos : 0 < dmCrossSectionRatio :=
  31  Jcost_pos_of_ne_one phi phi_pos phi_ne_one
  32
  33/-- The prediction is not yet excluded: cross-section is in J(phi) band. -/
  34theorem dmCrossSection_in_band : 0 < dmCrossSectionRatio ∧ dmCrossSectionRatio < 0.13 := by
  35  constructor
  36  · exact dmCrossSection_pos
  37  · unfold dmCrossSectionRatio
  38    rw [Constants.Jcost_phi_val]
  39    linarith [phi_lt_onePointSixTwo]
  40
  41structure DarkMatterXENONCert where
  42  dm_mass_ratio : dmMassRatio = 1 / 45
  43  cross_section_pos : 0 < dmCrossSectionRatio
  44  cross_section_band : 0 < dmCrossSectionRatio ∧ dmCrossSectionRatio < 0.13
  45
  46noncomputable def darkMatterXENONCert : DarkMatterXENONCert where
  47  dm_mass_ratio := rfl
  48  cross_section_pos := dmCrossSection_pos
  49  cross_section_band := dmCrossSection_in_band
  50
  51end IndisputableMonolith.Cosmology.DarkMatterXENONPrediction
  52