pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.Rotation

show as:
view Lean formalization →

The module defines a Newtonian rotation system pairing gravitational constant G with enclosed mass function Menc(r). It supplies derived rotation velocity vrot and acceleration g, plus lemmas establishing flat curves for linear Menc profiles. Galactic dynamics researchers cite it for the Newtonian limit identities. The module consists of definitions and direct algebraic lemmas with no complex proof structure.

claimA rotation system is given by gravitational constant $G$ and enclosed mass $M(r)$. Rotation velocity satisfies $v^2(r) = G M(r)/r$. For linear $M(r) = k r$ the velocity is constant (flat curve). Acceleration is $g(r) = G M(r)/r^2$.

background

The module sits inside the Gravity facade of Recognition Science and introduces the rotation system as the Newtonian baseline. RotSys pairs G with Menc; vrot extracts the circular velocity from the centripetal balance; g is the radial acceleration. Sibling definitions include vrot_sq, vrot_flat_of_linear_Menc and g_of_linear_Menc, all operating in the D=3 spatial setting with G expressed in phi-native units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Newtonian rotation identities that the Gravity facade re-exports and that RotationILG extends with ILG kernels. It anchors the flat-curve results used downstream for galactic dynamics and connects to the phi-ladder mass formula via the linear Menc case.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (7)