Gravity Rotation Vrot Sq

The rotation-curve identity

In Newtonian gravity, a small body in a circular orbit around a central mass feels a centripetal acceleration v²/r, where v is its orbital speed and r is the orbital radius. The gravitational acceleration pulling it inward is G M / r², with G Newton's constant and M the mass enclosed inside the orbit. Setting the two accelerations equal gives v² = G M / r, the standard rotation-curve formula. The Recognition Science declaration vrot_sq states exactly this identity as a formal lemma: for any rotation system with positive gravitational constant G and a nonnegative enclosed-mass function Menc, if the radius r is positive, then (vrot S r)² = G * Menc r / r.

The lemma is a definitional unpacking. The framework first defines a rotation system as a structure carrying G, a positivity proof, and a mass function Menc that is nonnegative at every radius. It then defines the rotation velocity vrot as the square root of G * Menc(r) / r. The lemma vrot_sq simply squares that definition and simplifies, using the fact that the square root of a nonnegative number squared is the number itself. The proof is a short chain of algebraic steps, all checked by the machine-checked library of formal theorems. It does not introduce any new physics; it formalizes the familiar Newtonian relation in the framework's own notation.

The same file proves a consequence that matters for galaxy observations. If the enclosed mass grows linearly with radius, Menc(r) = α r with α ≥ 0, then the rotation velocity becomes constant: vrot(r) = √(G α) for every positive r. That is the flat rotation curve. The framework states this as a separate lemma, vrot_flat_of_linear_Menc, and also gives a Newtonian version with a nonnegative slope γ. The centripetal acceleration then falls as g(r) = (G α)/r, so the constant speed is balanced by a declining acceleration.

What vrot_sq does not claim is just as important. It does not say that any real galaxy has a linearly growing enclosed mass; that is a hypothesis about mass distributions, not a theorem. It does not derive the flat rotation curve from dark matter or any modified gravity; it only shows what the Newtonian formula gives under a stated mass assumption. It does not claim that the rotation system's G is the measured gravitational constant; the structure allows any positive real G. Finally, the lemma is purely algebraic: it assumes circular motion and the centripetal acceleration formula, and it does not prove that orbits are stable or that the circular-orbit approximation holds.

/-- 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 lemma does not claim that any real galaxy has a linearly growing enclosed mass. The lemma does not derive the flat rotation curve from dark matter or modified gravity. The lemma does not assert that G is the measured gravitational constant, only that it is positive.

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: