vrot
Rotation velocity is defined for a system S at radius r by taking the square root of gravitational constant times enclosed mass divided by radius. Researchers studying galactic dynamics cite this when analyzing flat rotation curves under linear mass distributions. The implementation directly encodes the centripetal force balance without additional computation.
claim$v(r) = (G M(r)/r)^{1/2}$ where $G$ is the gravitational constant and $M(r)$ is the enclosed mass function of a rotation system.
background
A rotation system is a structure containing a positive real gravitational constant $G$ together with a non-negative function $Menc: ℝ → ℝ$ that returns the mass enclosed within radius $r$. The module Gravity.Rotation assembles the basic Newtonian expressions for orbital motion once $G$ and $Menc$ are supplied. Upstream constants supply the explicit RS-native value of $G$ obtained from the phi-forcing chain.
proof idea
The definition is a direct one-line assignment of the Newtonian orbital velocity formula.
why it matters in Recognition Science
This definition supplies the common starting point for the module's lemmas on flat rotation curves and centripetal acceleration. It feeds the downstream results vrot_sq, g, vrot_flat_of_linear_Menc and vrot_flat_of_linear_Menc_Newtonian, which recover the constant-velocity profile when enclosed mass grows linearly. The construction sits inside the Recognition Science treatment of gravity that derives $G$ from the phi-ladder and the eight-tick octave.
scope and limits
- Does not prescribe any particular functional form for the enclosed-mass function Menc(r).
- Does not incorporate relativistic or post-Newtonian corrections.
- Does not derive the numerical value of G from the phi-forcing chain inside this declaration.
formal statement (Lean)
15noncomputable def vrot (S : RotSys) (r : ℝ) : ℝ :=
proof body
Definition body.
16 Real.sqrt (S.G * S.Menc r / r)
17
18/-- Centripetal acceleration as a function of radius. -/