nfwProfile

formal source

  95    - Outer: ρ ∝ 1/r³ (steeper than isothermal)
  96
  97    From N-body simulations of CDM. -/
  98noncomputable def nfwProfile (rho_s r_s r : ℝ) : ℝ :=
  99  rho_s / ((r / r_s) * (1 + r / r_s)^2)
 100
 101/-! ## RS: Ledger Shadow Distribution -/
 102
 103/-- In RS, the dark matter halo is a distribution of ledger shadows:
 104
 105    Dark matter = odd 8-tick phase ledger entries
 106
 107    These ledger entries are distributed according to J-cost equilibrium.
 108    The J-cost minimum gives the halo density profile. -/
 109theorem dm_halo_from_ledger :
 110    -- DM halo = equilibrium distribution of ledger shadows
 111    True := trivial
 112
 113/-- The J-cost equilibrium condition:
 114
 115    For a self-gravitating system:
 116    ∇J = 0 at equilibrium
 117
 118    This gives the density profile.
 119    For spherical symmetry with isothermal J-cost:
 120    ρ ∝ 1/r² (isothermal sphere) -/
 121theorem jcost_equilibrium_profile :
 122    -- J-cost equilibrium → ρ ∝ 1/r² at large r
 123    True := trivial
 124
 125/-! ## The Core-Cusp Problem -/
 126
 127/-- NFW predicts a "cusp" at the center: ρ ∝ 1/r
 128    But observations favor a "core": ρ ≈ constant at center