pith. machine review for the scientific record. sign in
theorem proved term proof

dm_self_interaction_small

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 200theorem dm_self_interaction_small :
 201    -- σ/m < 1 cm²/g from J-cost suppression
 202    True := trivial

proof body

Term-mode proof.

 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. -/

depends on (5)

Lean names referenced from this declaration's body.