Gravity Rotation

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

THEOREM g_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean

THEOREM vrot_flat_of_linear_Menc · IndisputableMonolith/Gravity/Rotation.lean

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: