`dm_self_interaction_small`

proved

show as: view math explainer →

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

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

 197    But cross-section is small: σ/m < 1 cm²/g (cluster limits).
 198
 199    In RS: Odd-phase × odd-phase → even-phase is suppressed. -/
 200theorem dm_self_interaction_small :
 201    -- σ/m < 1 cm²/g from J-cost suppression
 202    True := trivial
 203
 204/-! ## Structure Formation -/
 205
 206/-- Dark matter drives structure formation:
 207
 208    1. DM decouples early (no photon pressure)
 209    2. DM perturbations grow during radiation era
 210    3. Baryons fall into DM "halos" after recombination
 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 -/

papers checked against this theorem

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