def
definition
dm_baryon_ratio
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 66.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
63noncomputable def omega_b : ℝ := 0.05
64
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)",