IndisputableMonolith.Gravity.Rotation

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Gravity
   5namespace Rotation
   6
   7/-- Rotation system with gravitational constant G and enclosed mass function `Menc`. -/
   8structure RotSys where
   9  G : ℝ
  10  posG : 0 < G
  11  Menc : ℝ → ℝ
  12  nonnegM : ∀ r, 0 ≤ Menc r
  13
  14/-- Rotation velocity as a function of radius. -/
  15noncomputable def vrot (S : RotSys) (r : ℝ) : ℝ :=
  16  Real.sqrt (S.G * S.Menc r / r)
  17
  18/-- Centripetal acceleration as a function of radius. -/
  19noncomputable def g (S : RotSys) (r : ℝ) : ℝ :=
  20  (vrot S r) ^ 2 / r
  21
  22/-- Algebraic identity: `vrot^2 = G Menc / r` for `r > 0`. -/
  23lemma vrot_sq (S : RotSys) {r : ℝ} (hr : 0 < r) :
  24  (vrot S r) ^ 2 = S.G * S.Menc r / r := by
  25  dsimp [vrot]
  26  have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
  27    have hM : 0 ≤ S.Menc r := S.nonnegM r
  28    exact mul_nonneg (le_of_lt S.posG) hM
  29  have hfrac_nonneg : 0 ≤ S.G * S.Menc r / r := by
  30    exact div_nonneg hnum_nonneg (le_of_lt hr)
  31  calc
  32    (Real.sqrt (S.G * S.Menc r / r)) ^ 2 = S.G * S.Menc r / r := by
  33      rw [Real.sq_sqrt hfrac_nonneg]
  34
  35/-- If the enclosed mass grows linearly, `Menc(r) = α r` with `α ≥ 0`, then the rotation curve is flat:
  36    `vrot(r) = √(G α)` for all `r > 0`. -/
  37lemma vrot_flat_of_linear_Menc (S : RotSys) (α : ℝ)
  38  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :
  39  ∀ {r : ℝ}, 0 < r → vrot S r = Real.sqrt (S.G * α) := by
  40  intro r hr
  41  have hM : S.Menc r = α * r := hlin hr
  42  have hrne : r ≠ 0 := ne_of_gt hr
  43  have hfrac : S.G * S.Menc r / r = S.G * α := by
  44    calc
  45      S.G * S.Menc r / r = S.G * (α * r) / r := by rw [hM]
  46      _ = S.G * α * r / r := by ring
  47      _ = S.G * α := by field_simp [hrne]
  48  dsimp [vrot]
  49  rw [hfrac]
  50
  51/-- Under linear mass growth `Menc(r) = α r`, the centripetal acceleration scales as `g(r) = (G α)/r`. -/
  52lemma g_of_linear_Menc (S : RotSys) (α : ℝ)
  53  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :
  54  ∀ {r : ℝ}, 0 < r → g S r = (S.G * α) / r := by
  55  intro r hr
  56  have hM : S.Menc r = α * r := hlin hr
  57  have hrne : r ≠ 0 := ne_of_gt hr
  58  dsimp [g]
  59  have hvrot_sq : (vrot S r) ^ 2 = S.G * α := by
  60    have hfrac : S.G * S.Menc r / r = S.G * α := by
  61      calc
  62        S.G * S.Menc r / r = S.G * (α * r) / r := by rw [hM]
  63        _ = S.G * α * r / r := by ring
  64        _ = S.G * α := by field_simp [hrne]
  65    dsimp [vrot]
  66    have hnonneg : 0 ≤ S.G * S.Menc r / r := by
  67      have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
  68        have hM : 0 ≤ S.Menc r := S.nonnegM r
  69        exact mul_nonneg (le_of_lt S.posG) hM
  70      exact div_nonneg hnum_nonneg (le_of_lt hr)
  71    calc
  72      Real.sqrt (S.G * S.Menc r / r) ^ 2 = S.G * S.Menc r / r := by
  73        rw [Real.sq_sqrt hnonneg]
  74      _ = S.G * α := by rw [hfrac]
  75  calc
  76    g S r = (vrot S r) ^ 2 / r := by dsimp [g]
  77    _ = (S.G * α) / r := by rw [hvrot_sq]
  78
  79/-- Newtonian rotation curve is flat when the enclosed mass grows linearly:
  80    if `Menc(r) = γ r` (γ ≥ 0) then `vrot(r) = √(G γ)` for all r > 0. -/
  81lemma vrot_flat_of_linear_Menc_Newtonian (S : RotSys) (γ : ℝ)
  82  (hγ : 0 ≤ γ) (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = γ * r) :
  83  ∀ {r : ℝ}, 0 < r → vrot S r = Real.sqrt (S.G * γ) := by
  84  intro r hr
  85  have hrne : r ≠ 0 := ne_of_gt hr
  86  have hM : S.Menc r = γ * r := hlin hr
  87  -- vrot = sqrt(G * Menc / r) = sqrt(G * γ)
  88  have hnonneg : 0 ≤ S.G * γ := mul_nonneg (le_of_lt S.posG) hγ
  89  have hfrac : S.G * S.Menc r / r = S.G * γ := by
  90    calc
  91      S.G * S.Menc r / r = S.G * (γ * r) / r := by rw [hM]
  92      _ = S.G * γ * r / r := by ring
  93      _ = S.G * γ := by field_simp [hrne]
  94  dsimp [vrot]
  95  rw [hfrac]
  96
  97end Rotation
  98end Gravity
  99end IndisputableMonolith