Gravity Rotation G Of Linear Menc

A flat rotation curve's gravity

In Newtonian gravity, a body on a circular orbit feels a centripetal acceleration v²/r, and for that orbit to be stable the gravitational pull must supply exactly that acceleration. If the enclosed mass M(r) inside radius r grows linearly, M(r) = α r, then the orbital speed v = √(G M(r)/r) becomes √(G α), a constant independent of r. That is the flat rotation curve: outer parts of a disk orbit just as fast as inner parts. The same assumption makes the centripetal acceleration g(r) = v²/r equal to (G α)/r, so the required inward pull falls off as one over radius, not as one over radius squared.

The machine-checked library of formal theorems records this as a proved lemma, g_of_linear_Menc, inside its rotation module. The library defines a rotation system as a gravitational constant G, a positive-mass condition, and an enclosed-mass function M(r) that is never negative. From those definitions it proves, for any positive radius, the identity v² = G M(r)/r, and then the flat-curve and inverse-radius consequences under the linear-growth assumption. The proof is a short algebraic chain: it squares the square root, uses the nonnegativity of G and M(r) to justify the step, and divides through by r. Nothing about dark matter, disk stability, or observed galaxies enters the statement; it is a conditional fact about a defined mathematical model.

The lemma does not claim that real galaxies have linearly growing enclosed mass. It states an implication: if M(r) = α r for all positive r, then the acceleration has the 1/r form. The converse also is not claimed; a flat rotation curve does not force linear mass growth, since other mass profiles can produce the same speed law. Nor does the library claim that this acceleration law is observed; it is a derived consequence inside a model whose inputs are chosen by the user. The value of the result is that it isolates exactly what the linear-mass assumption buys: a constant orbital speed and an inverse-radius acceleration, two signatures that observers can look for in data.

In the Recognition Science framework, this lemma is one small rung in a larger structure, but it stands on its own as a piece of classical Newtonian kinematics. A reader who wants to know what a flat rotation curve implies about the gravitational field can take the 1/r acceleration directly from this result, and a reader who wants to check the framework's internal consistency can see that the library's definitions reproduce a standard textbook identity without extra assumptions.

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

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

/-- Rotation system with gravitational constant G and enclosed mass function `Menc`. -/
structure RotSys where
  G : ℝ
  posG : 0 < G
  Menc : ℝ → ℝ
  nonnegM : ∀ r, 0 ≤ Menc r

What this page does not claim

The lemma does not assert that any real galaxy has linearly growing enclosed mass. The lemma does not prove that a flat rotation curve implies linear mass growth. The lemma makes no claim about dark matter or about observed galaxy dynamics.

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: