dmIsNot

formal source

  91    - Black holes (mostly) - microlensing limits
  92    - Neutrinos (mostly) - too hot for structure
  93    - Modified gravity (alone) - cluster data -/
  94def dmIsNot : List String := [
  95  "MACHOs (ruled out for most mass range)",
  96  "Primordial black holes (limited)",
  97  "Hot dark matter (neutrinos - too fast)",
  98  "MOND alone (doesn't fit clusters)"
  99]
 100
 101/-! ## Standard Candidates -/
 102
 103/-- WIMPs: Weakly Interacting Massive Particles
 104    - Mass: ~10-1000 GeV
 105    - Interaction: Weak-scale
 106    - Thermal relic: Ω_dm from freeze-out
 107    - Status: NOT found despite decades of searches -/
 108structure WIMP where
 109  mass : ℝ  -- GeV
 110  cross_section : ℝ  -- cm²
 111  thermal_relic : Bool
 112
 113/-- Axions: Very light pseudoscalars
 114    - Mass: ~10⁻⁶-10⁻³ eV
 115    - From PQ solution to strong CP
 116    - Misalignment production
 117    - Status: Actively searched -/
 118structure Axion where
 119  mass : ℝ  -- eV
 120  decay_constant : ℝ  -- GeV
 121
 122/-- Primordial black holes: BHs from early universe
 123    - Mass range: 10⁻¹⁸-10⁵ M_sun (windows remain)
 124    - Form from density perturbations