Gravity Rotation Rot Sys

Rotation curves

A rotation curve is the graph of orbital speed against distance from the center of a galaxy or other mass. In Newtonian gravity, a test particle at radius r orbiting a central mass M has speed v = sqrt(GM/r), where G is the gravitational constant. The declaration RotSys (a formal structure in the framework's machine-checked library of formal theorems) packages exactly this setup as three assumptions: a positive gravitational constant G, an enclosed mass function Menc(r), and the condition that enclosed mass is never negative. From these it defines the rotation velocity vrot(r) = sqrt(G * Menc(r) / r) and the centripetal acceleration g(r) = vrot(r)^2 / r.

The central result is a theorem about what happens when the enclosed mass grows linearly with radius, Menc(r) = α r for a constant α ≥ 0. Then the rotation curve is flat: vrot(r) = sqrt(G α) for every r > 0. In words, if the mass inside radius r increases in direct proportion to r, the orbital speed stops depending on r and becomes constant. The same assumption makes the centripetal acceleration fall off as g(r) = (G α) / r. Both statements are proved in the library, and the proof of the speed identity vrot^2 = G Menc / r for r > 0 is also checked.

This is a classical result, not a new prediction. It is the standard Newtonian explanation for why spiral galaxy rotation curves stay flat at large radii: the enclosed mass must be growing roughly linearly, which in observed galaxies is attributed to dark matter halos. The framework's contribution is formal, not physical: it states the assumptions cleanly and verifies the algebra in a machine-checked library. The declaration does not assert that real galaxies have linear mass profiles, does not introduce dark matter, and does not derive the value of G. It only establishes what follows from the stated premises.

In Recognition Science, this structure is a vocabulary for rotation in gravitational settings, but it is deliberately minimal. It contains no claim about the origin of gravity, no derivation of the gravitational constant from the framework's forcing chain, and no statement about the number of spatial dimensions. The theorems are conditional: given a RotSys whose enclosed mass is linear, the flat curve follows. Whether any physical system satisfies that condition is a separate question the declaration leaves open.

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

/-- 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]

/-- 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]

What this page does not claim

RotSys does not claim that real galaxies have linearly growing enclosed mass. RotSys does not derive the value of the gravitational constant G. RotSys does not introduce or explain dark matter.

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: