`mondAcceleration`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.GalaxyRotation on GitHub at line 163.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 179
 180    This may be a cosmological coincidence... or not.
 181
 182    In RS: a₀ may be set by φ-ladder timescales. -/
 183theorem mond_acceleration_phi :
 184    -- a₀ may relate to φ-ladder
 185    True := trivial
 186
 187/-! ## Baryonic Tully-Fisher -/
 188
 189/-- The baryonic Tully-Fisher relation is VERY tight:
 190    M_baryon ∝ v⁴
 191
 192    Scatter is remarkably small (< 0.1 dex).
 193    This suggests a fundamental relationship.

papers checked against this theorem

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