pith. machine review for the scientific record. sign in
theorem proved term proof

mond_acceleration_phi

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 183theorem mond_acceleration_phi :
 184    -- a₀ may relate to φ-ladder
 185    True := trivial

proof body

Term-mode proof.

 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. -/

depends on (5)

Lean names referenced from this declaration's body.