pith. machine review for the scientific record. sign in
def definition def or abbrev

structureFormation

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)

 214def structureFormation : List String := [

proof body

Definition body.

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

depends on (2)

Lean names referenced from this declaration's body.