WIMP

formal source

 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
 125    - Status: Some windows still open -/
 126structure PBH where
 127  mass : ℝ  -- Solar masses
 128  formation_epoch : String
 129
 130/-! ## RS: Ledger Shadows -/
 131
 132/-- In RS, dark matter = "ledger shadows":
 133
 134    The ledger has different "sectors" based on 8-tick phase:
 135    - **Visible sector**: Phases that couple to photons
 136    - **Dark sector**: Phases that don't couple to photons
 137
 138    Both gravitate (J-cost couples universally to geometry).