coreCuspProblem

formal source

 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
 152/-! ## MOND Alternative -/
 153
 154/-- Modified Newtonian Dynamics (MOND):
 155
 156    At low accelerations (a < a₀ ~ 10⁻¹⁰ m/s²):
 157    The effective gravitational force is enhanced:
 158    F = ma√(a/a₀) instead of F = ma
 159
 160    This gives flat rotation curves WITHOUT dark matter!
 161
 162    But: MOND fails for galaxy clusters and CMB. -/
 163noncomputable def mondAcceleration : ℝ := 1.2e-10  -- m/s²
 164
 165/-- The Tully-Fisher relation:
 166    L ∝ v⁴ (luminosity scales as 4th power of rotation velocity)