Encyclopedia Gravity Gravity Rotation

ARTICLE 3 claims 3 theorems

Gravity Rotation

Gravity rotation is the velocity profile of a body in circular orbit under a central gravitational field, and the module proves that a linearly growing enclosed mass forces a flat rotation curve.

Verify this page

Rotation curves

Gravity rotation is the study of orbital rotation curves: the speed at which a body must move to stay in a circular orbit at a given radius around a central mass. In Recognition Science the subject is formalized as a rotation system, a structure that pairs a gravitational constant G with an enclosed mass function Menc(r), the mass inside radius r. The module defines the rotation velocity vrot(r) as the square root of G times Menc(r) divided by r, the standard Newtonian balance between gravity and centripetal acceleration.

The central result is a forced consequence of that definition. If the enclosed mass grows linearly with radius, meaning Menc(r) equals some constant α times r, then the rotation velocity is constant: vrot(r) equals the square root of G times α for every positive radius. The module proves this as a theorem. The same linear-mass condition also forces the centripetal acceleration to fall off as 1/r, which is the inverse-radius scaling that accompanies a flat curve.

This is the same mathematical fact that appears in galaxy observations: a flat rotation curve, where outer stars move at the same speed as inner ones, follows from a mass distribution that grows linearly outward. The module does not assert that real galaxies have such mass distributions. It proves the conditional statement: given that distribution, the curve is flat. The theorem is a piece of the Recognition Science library that connects the framework's forced constants and structures to a standard result in classical gravitational dynamics.

THEOREM vrot_flat_of_linear_Menc · vrot_flat_of_linear_Menc_Newtonian · IndisputableMonolith/Gravity/Rotation.lean
vrot_flat_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean:35 
/-- 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]
vrot_flat_of_linear_Menc_Newtonian · IndisputableMonolith/Gravity/Rotation.lean:79 
/-- 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]
THEOREM g_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean
g_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean:51 
/-- 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]
THEOREM vrot_flat_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean
vrot_flat_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean:35 
/-- 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]

What this page does not claim

This answer does not claim that real galaxies have linearly growing enclosed mass. This answer does not claim that Recognition Science derives the measured rotation curves of specific galaxies. This answer does not claim that the rotation module introduces new physics beyond the standard Newtonian balance.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND