pith. machine review for the scientific record. sign in
def definition def or abbrev

milkyWayData

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)

  72def milkyWayData : List (String × String) := [

proof body

Definition body.

  73  ("Solar radius", "8 kpc, v ≈ 220 km/s"),
  74  ("Outer disk", "20 kpc, v ≈ 220 km/s"),
  75  ("Expected from visible", "v ≈ 150 km/s at 20 kpc"),
  76  ("Missing mass", "Factor of ~2 at 20 kpc")
  77]
  78
  79/-! ## Dark Matter Halo -/
  80
  81/-- To get v = constant, we need M(r) ∝ r:
  82    v² = G M(r) / r
  83    v = constant → M(r) ∝ r
  84
  85    This requires ρ(r) ∝ 1/r²:
  86    M(r) = ∫ 4πr² ρ(r) dr = ∫ 4πr² × (ρ₀/r²) dr = 4πρ₀ r -/

depends on (15)

Lean names referenced from this declaration's body.