Gravity Rotation Vrot Flat Of Linear Menc Newtonian

Flat rotation curves

In Newtonian gravity, the orbital speed of a star around a central mass depends on how much mass lies inside its orbit. For a point mass, speed falls as the square root of distance. But if the enclosed mass grows linearly with radius, so that Menc(r) = γ r for a constant γ, then the speed becomes vrot(r) = √(Gγ), independent of r. This is the flat rotation curve: all stars move at the same speed, no matter how far out they orbit.

The result is a theorem in the framework's machine-checked library of formal theorems. It starts from a rotation system, a structure with a gravitational constant G and an enclosed mass function Menc(r), and assumes Menc(r) = γ r with γ ≥ 0 for all positive radii. Under that assumption, the library proves that the rotation velocity vrot(r), defined as √(G Menc(r)/r), equals √(Gγ) for every r > 0. A companion theorem shows the centripetal acceleration then scales as (Gγ)/r, so the acceleration falls off while the speed stays flat.

The proof is a direct algebraic identity: squaring the definition of vrot gives vrot² = G Menc(r)/r, and substituting the linear mass law yields vrot² = Gγ. The theorem requires γ to be nonnegative, which keeps the square root real. It does not require any particular value of G or γ; the flatness holds for any nonnegative linear mass profile.

In Recognition Science, this theorem is a building block, not a physical discovery. The framework proves the mathematical consequence of a linear mass assumption, but it does not claim that real galaxies have such mass profiles. The theorem says nothing about dark matter, modified gravity, or why observed rotation curves are flat. Those questions remain open targets for the framework, not results it has derived.

/-- Newtonian rotation curve is flat when the enclosed mass grows linearly:
    if `Menc(r) = γ r` (γ ≥ 0) then `vrot(r) = √(G γ)` for all r > 0. -/
lemma vrot_flat_of_linear_Menc_Newtonian (S : RotSys) (γ : ℝ)
  (hγ : 0 ≤ γ) (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = γ * r) :
  ∀ {r : ℝ}, 0 < r → vrot S r = Real.sqrt (S.G * γ) := by
  intro r hr
  have hrne : r ≠ 0 := ne_of_gt hr
  have hM : S.Menc r = γ * r := hlin hr
  -- vrot = sqrt(G * Menc / r) = sqrt(G * γ)
  have hnonneg : 0 ≤ S.G * γ := mul_nonneg (le_of_lt S.posG) hγ
  have hfrac : S.G * S.Menc r / r = S.G * γ := by
    calc
      S.G * S.Menc r / r = S.G * (γ * r) / r := by rw [hM]
      _ = S.G * γ * r / r := by ring
      _ = S.G * γ := by field_simp [hrne]
  dsimp [vrot]
  rw [hfrac]

/-- Rotation velocity as a function of radius. -/
noncomputable def vrot (S : RotSys) (r : ℝ) : ℝ :=
  Real.sqrt (S.G * S.Menc r / r)

/-- Under linear mass growth `Menc(r) = α r`, the centripetal acceleration scales as `g(r) = (G α)/r`. -/
lemma g_of_linear_Menc (S : RotSys) (α : ℝ)
  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :
  ∀ {r : ℝ}, 0 < r → g S r = (S.G * α) / r := by
  intro r hr
  have hM : S.Menc r = α * r := hlin hr
  have hrne : r ≠ 0 := ne_of_gt hr
  dsimp [g]
  have hvrot_sq : (vrot S r) ^ 2 = S.G * α := by
    have hfrac : S.G * S.Menc r / r = S.G * α := by
      calc
        S.G * S.Menc r / r = S.G * (α * r) / r := by rw [hM]
        _ = S.G * α * r / r := by ring
        _ = S.G * α := by field_simp [hrne]
    dsimp [vrot]
    have hnonneg : 0 ≤ S.G * S.Menc r / r := by
      have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
        have hM : 0 ≤ S.Menc r := S.nonnegM r
        exact mul_nonneg (le_of_lt S.posG) hM
      exact div_nonneg hnum_nonneg (le_of_lt hr)
    calc
      Real.sqrt (S.G * S.Menc r / r) ^ 2 = S.G * S.Menc r / r := by
        rw [Real.sq_sqrt hnonneg]
      _ = S.G * α := by rw [hfrac]
  calc
    g S r = (vrot S r) ^ 2 / r := by dsimp [g]
    _ = (S.G * α) / r := by rw [hvrot_sq]

What this page does not claim

The theorem does not claim that real galaxies have linear mass profiles. It does not explain why observed rotation curves are flat. It does not address dark matter or modified gravity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Rotation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: