IndisputableMonolith.Gravity.Rotation
The Gravity.Rotation module defines a rotation system RotSys parameterized by gravitational constant G and enclosed mass function Menc. Physicists working on galactic dynamics or flat rotation curves would cite its Newtonian identities. It supplies the baseline for the Gravity facade re-export and the RotationILG extension. The module consists of definitions and lemmas establishing v² = GM/r together with flat-curve results for linear Menc.
claimA rotation system is a pair $(G, M_{ m enc})$ with $G$ the gravitational constant and $M_{ m enc}(r)$ the enclosed mass at radius $r$, inducing rotation velocity satisfying $v_{ m rot}^2(r) = G M_{ m enc}(r)/r$ and acceleration $g(r) = G M_{ m enc}(r)/r^2$, plus derived flat-curve identities when $M_{ m enc}$ is linear.
background
The module introduces the rotation system structure together with the functions vrot, g, vrot_sq and the lemmas vrot_flat_of_linear_Menc, g_of_linear_Menc. It works in the Newtonian limit where the inverse-square law holds and enclosed mass determines orbital speed. The setting is the gravity formalization re-exported by the parent Gravity module, which also contains ILG time kernels and HSB suppression factors.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the Newtonian rotation curve identities (v² = GM/r, flat curves) re-exported by the Gravity facade. It is imported by RotationILG to extend the same objects to information-limited gravity. This places the classical baseline inside the Recognition Science gravity formalization before ILG and DerivedFactors layers are added.
scope and limits
- Does not incorporate general-relativistic corrections to orbital motion.
- Does not specify Menc beyond the linear case used for flat curves.
- Does not derive the numerical value of G from phi-ladder or RCL relations.
- Does not treat time-dependent or non-axisymmetric mass distributions.