dm_halo_from_ledger

formal source

 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
 129
 130    This is the "core-cusp problem."
 131
 132    Possible solutions:
 133    1. Baryonic feedback
 134    2. Self-interacting dark matter
 135    3. RS: Ledger interactions at high density -/
 136def coreCuspProblem : String :=
 137  "Simulations predict cusp (ρ ∝ 1/r), observations favor core (ρ = const)"
 138
 139/-- RS perspective on core-cusp: