`structureFormation`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.DarkMatter
domain: Cosmology
line: 214 · 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 214.

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

 211    4. Galaxies form in DM potential wells
 212
 213    Without DM, galaxies wouldn't have formed in time. -/
 214def structureFormation : List String := [
 215  "DM decouples early (z ~ 10⁶)",
 216  "DM perturbations grow: δ ∝ a",
 217  "Baryons fall in after z ~ 1100",
 218  "Galaxies form in DM halos"
 219]
 220
 221/-! ## Detection? -/
 222
 223/-- Can ledger shadows be detected?
 224
 225    1. **Gravitational**: Already detected (rotation curves, etc.)
 226    2. **Direct detection**: Scattering off nuclei - difficult
 227       (Odd-phase doesn't couple well to even-phase)
 228    3. **Indirect**: Annihilation products - possible
 229       (Odd + odd → even, produces visible particles)
 230    4. **Collider**: Produce at LHC - no luck so far -/
 231def detectionMethods : List String := [
 232  "Gravitational (confirmed)",
 233  "Direct detection (ongoing)",
 234  "Indirect detection (cosmic rays)",
 235  "Collider production (none yet)"
 236]
 237
 238/-- RS prediction for direct detection:
 239
 240    Cross-section suppressed by phase mismatch.
 241    σ ~ σ_weak × (phase mismatch factor)
 242
 243    This explains null results so far! -/
 244theorem rs_explains_null_detection :

papers checked against this theorem

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