`detectionMethods`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 231.

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

 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 :
 245    -- Odd-even phase mismatch suppresses detection
 246    True := trivial
 247
 248/-! ## Alternative: MOND? -/
 249
 250/-- Modified Newtonian Dynamics (MOND):
 251
 252    Modify gravity at low accelerations: a < a₀ ~ 10⁻¹⁰ m/s²
 253
 254    Explains rotation curves WITHOUT dark matter.
 255    But: Fails for clusters, CMB, structure formation.
 256
 257    RS: Dark matter is real, not modified gravity. -/
 258def mondStatus : String :=
 259  "Works for rotation curves, fails for clusters and CMB"
 260
 261/-! ## Summary -/

papers checked against this theorem

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