Gravity Rotation Vrot

The rotation velocity

The rotation velocity vrot is the speed at which a star or gas cloud orbits the center of a galaxy, assuming a circular path. In the framework's machine-checked library of formal theorems, vrot is defined as the square root of the gravitational constant times the enclosed mass divided by the radius: vrot(r) = √(G · Menc(r) / r). Here G is the gravitational constant, and Menc(r) is the total mass contained within a sphere of radius r from the center. The definition is a direct translation of Newton's law of gravitation into a computable function on real numbers.

The library proves two standard consequences. First, the square of the rotation velocity equals G times the enclosed mass divided by the radius, for any positive radius. This is just a restatement of the definition, but the library checks it formally. Second, if the enclosed mass grows linearly with radius, meaning Menc(r) = αr for some nonnegative constant α, then the rotation curve is flat: vrot(r) equals the constant √(Gα) for all radii. This is the classic result that explains why galaxies with mass distributed in a disk or halo show a rotation speed that does not drop off with distance.

The same flatness result appears again under a Newtonian label, with the mass coefficient called γ instead of α. The library proves it with the same method, showing the conclusion holds whenever the mass grows linearly and the coefficient is nonnegative. The centripetal acceleration, defined as the square of the velocity divided by the radius, then scales as (Gα)/r under the same linear mass assumption.

In Recognition Science, this declaration is a small piece of the framework's effort to derive classical physics from its own axioms. The framework models gravity as a rotation system with a gravitational constant and a mass function, and vrot is the rotation speed that follows. The library proves the algebraic identity and the flatness cases as theorems, but it does not derive the gravitational constant itself, nor does it explain why galaxies have linear mass distributions. Those questions remain outside the scope of this particular declaration.

The practical value of vrot is that it gives astronomers a clean way to connect observed rotation speeds to mass estimates. A flat rotation curve, measured in real galaxies, implies a mass that grows linearly with radius, which is one of the key pieces of evidence for dark matter. The framework's formal proof of the flatness case confirms that the mathematics behind that inference is sound, even though the framework itself does not take a position on what the unseen mass is.

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

/-- Algebraic identity: `vrot^2 = G Menc / r` for `r > 0`. -/
lemma vrot_sq (S : RotSys) {r : ℝ} (hr : 0 < r) :
  (vrot S r) ^ 2 = S.G * S.Menc r / r := by
  dsimp [vrot]
  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
  have hfrac_nonneg : 0 ≤ S.G * S.Menc r / r := by
    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 hfrac_nonneg]

/-- If the enclosed mass grows linearly, `Menc(r) = α r` with `α ≥ 0`, then the rotation curve is flat:
    `vrot(r) = √(G α)` for all `r > 0`. -/
lemma vrot_flat_of_linear_Menc (S : RotSys) (α : ℝ)
  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :
  ∀ {r : ℝ}, 0 < r → vrot S r = Real.sqrt (S.G * α) := by
  intro r hr
  have hM : S.Menc r = α * r := hlin hr
  have hrne : r ≠ 0 := ne_of_gt hr
  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]

/-- 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 declaration does not derive the value of the gravitational constant G. The declaration does not explain why galaxies have linear mass distributions. The declaration does not take a position on what the unseen mass in galaxies is.

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: