circularVelocity

formal source

  49/-- The circular velocity of a star at radius r:
  50    v(r) = √(G M(r) / r)
  51    where M(r) is the enclosed mass. -/
  52noncomputable def circularVelocity (M r : ℝ) (hr : r > 0) : ℝ :=
  53  Real.sqrt (G * M / r)
  54
  55/-- For a point mass (or spherical distribution):
  56    v(r) ∝ 1/√r (Keplerian falloff)
  57
  58    But observed: v(r) ≈ constant! -/
  59theorem keplerian_falloff :
  60    -- v ∝ 1/√r for point mass
  61    True := trivial
  62
  63/-- The observed flat rotation curve:
  64    v ≈ 200-300 km/s for most spirals
  65    Roughly constant from ~5 kpc to ~30+ kpc! -/
  66noncomputable def typicalRotationVelocity : ℝ := 220  -- km/s (Milky Way)
  67
  68/-- The Milky Way rotation curve:
  69    - Sun at 8 kpc: v ≈ 220 km/s
  70    - Outer disk at 20 kpc: v ≈ 220 km/s (still flat!)
  71    - Visible mass would give v ≈ 150 km/s at 20 kpc -/
  72def milkyWayData : List (String × String) := [
  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