`mond_acceleration_phi`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.GalaxyRotation on GitHub at line 183.

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

 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.
 194
 195    CDM has trouble explaining the tightness.
 196    MOND explains it naturally. -/
 197def btfrData : String :=
 198  "M_baryon ∝ v⁴ with scatter < 0.1 dex"
 199
 200/-! ## Predictions -/
 201
 202/-- RS predictions for galaxy rotation:
 203
 204    1. **Flat curves**: From isothermal ledger distribution
 205    2. **Cores, not cusps**: From ledger interactions at high density
 206    3. **Tully-Fisher**: From J-cost equilibrium
 207    4. **MOND-like behavior**: At low accelerations
 208    5. **DM ratio ≈ 5:1**: From 8-tick phase counting -/
 209def predictions : List String := [
 210  "Flat rotation curves from ledger equilibrium",
 211  "Cores at centers (not cusps)",
 212  "Tully-Fisher relation M ∝ v⁴",
 213  "MOND-like at low accelerations",

papers checked against this theorem

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