`dmEvidence`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.DarkMatter
domain: Cosmology
line: 79 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  76    3. Gravitational lensing
  77    4. CMB anisotropies
  78    5. Structure formation -/
  79def dmEvidence : List String := [
  80  "Galaxy rotation curves (flat, not Keplerian)",
  81  "Galaxy cluster mass (10× visible)",
  82  "Gravitational lensing (mass maps)",
  83  "CMB acoustic peaks (matter content)",
  84  "Structure formation (need seeds)"
  85]
  86
  87/-! ## What Dark Matter Is NOT -/
  88
  89/-- Dark matter is NOT:
  90    - Ordinary matter (baryons) - BBN limits
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.