`rs_predicts_core`

proved

show as: view math explainer →

module: IndisputableMonolith.Cosmology.GalaxyRotation
domain: Cosmology
line: 148 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.GalaxyRotation on GitHub at line 148.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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)
 167
 168    MOND predicts this naturally.
 169    CDM requires it to arise from galaxy formation. -/
 170theorem tully_fisher :
 171    -- L ∝ v⁴ observed and predicted by MOND
 172    True := trivial
 173
 174/-- RS perspective on MOND:
 175
 176    The MOND acceleration scale a₀ ~ 10⁻¹⁰ m/s² is curious.
 177
 178    a₀ ~ cH₀ ~ c²/R_universe

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.