jcost_equilibrium_profile

formal source

 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:
 140
 141    At high density (galaxy center):
 142    - Ledger entries interact more strongly
 143    - J-cost rises faster than 1/r²
 144    - This prevents infinite cusp
 145    - Result: Core, not cusp!
 146
 147    This is a prediction of RS. -/
 148theorem rs_predicts_core :
 149    -- High-density ledger interactions → core, not cusp
 150    True := trivial
 151