`dm_is_dominant`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 68.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  65/-- The dark to baryon ratio. -/
  66noncomputable def dm_baryon_ratio : ℝ := omega_dm / omega_b
  67
  68theorem dm_is_dominant :
  69    dm_baryon_ratio > 5 := by
  70  unfold dm_baryon_ratio omega_dm omega_b
  71  norm_num
  72
  73/-- Evidence for dark matter:
  74    1. Galaxy rotation curves (Rubin 1970s)
  75    2. Galaxy cluster dynamics (Zwicky 1930s)
  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)"

papers checked against this theorem

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