IndisputableMonolith.Gravity.Rotation
The module defines a rotation system equipped with gravitational constant G and enclosed mass function Menc, together with derived quantities vrot and g. Researchers working on Newtonian limits of galactic dynamics or Recognition Science rotation curves would cite these identities. It is a definition module consisting of structures and basic algebraic identities with no proof obligations.
claimA rotation system is given by gravitational constant $G$ and enclosed mass function $M_{\rm enc}(r)$. It induces rotation velocity $v_{\rm rot}(r)$ and field strength $g(r)$ satisfying $v_{\rm rot}^2 = G M_{\rm enc}(r)/r$ along with the flat-curve case for linear $M_{\rm enc}$.
background
The module sits in the Gravity domain and imports only Mathlib. It introduces the structure RotSys packaging $G$ and the cumulative interior mass $M_{\rm enc}(r)$. Sibling definitions supply $v_{\rm rot}$, $g$, $v_{\rm rot_sq}$ and specialized identities for linear $M_{\rm enc}$ that recover flat rotation curves. The setting is the Newtonian rotation-curve layer that precedes Information-Limited Gravity extensions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the Newtonian rotation-curve identities re-exported by the parent Gravity facade. It is imported by Gravity.RotationILG to support the ILG time-kernel layer. The definitions anchor the formalization of $v^2 = GM/r$ and flat curves inside the Recognition framework.
scope and limits
- Does not incorporate relativistic corrections or general relativity.
- Does not derive the numerical value of G from the phi-ladder.
- Does not treat time-dependent or non-spherical mass distributions.
- Does not include quantum or Information-Limited Gravity kernels.