isothermal_halo

formal source

  84
  85    This requires ρ(r) ∝ 1/r²:
  86    M(r) = ∫ 4πr² ρ(r) dr = ∫ 4πr² × (ρ₀/r²) dr = 4πρ₀ r -/
  87theorem isothermal_halo :
  88    -- ρ ∝ 1/r² gives flat rotation curve
  89    True := trivial
  90
  91/-- The NFW (Navarro-Frenk-White) profile:
  92    ρ(r) = ρ_s / [(r/r_s)(1 + r/r_s)²]
  93
  94    - Inner: ρ ∝ 1/r (cuspy)
  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