vrot
plain-language theorem explainer
The definition supplies the Newtonian rotation velocity v(r) = sqrt(G * Menc(r) / r) for any rotation system S with positive G and nonnegative enclosed mass. Galaxy dynamicists and Recognition Science gravity derivations cite it when analyzing rotation curves. The implementation is a direct algebraic expression implementing centripetal balance.
Claim. For a rotation system $S$ with gravitational constant $G_S > 0$ and enclosed-mass function $M_S(r) : ℝ → ℝ$ satisfying $M_S(r) ≥ 0$ for all $r$, the rotation velocity is $v(S,r) := √(G_S · M_S(r) / r)$.
background
A rotation system is the structure RotSys containing a real number G > 0 together with a function Menc : ℝ → ℝ that returns nonnegative values. The module Gravity.Rotation sets up Newtonian rotation curves inside the Recognition Science gravity framework, taking G from the upstream Constants module (derived as λ_rec² c³ / (π ℏ)). Upstream results include the nuclear-density structure from NucleosynthesisTiers and the G reparametrization from Cost.FunctionalEquation, but the immediate dependencies are the constant G and the ledger factorization.
proof idea
The definition is a one-line wrapper that applies Real.sqrt directly to the Newtonian expression (S.G * S.Menc r / r).
why it matters
This definition is the base object for the centripetal acceleration g and for the lemmas vrot_sq, vrot_flat_of_linear_Menc and g_of_linear_Menc. It occupies the entry point of the Gravity.Rotation module and connects the Recognition Science derivation of G to observed galactic rotation curves. Downstream results use it to prove that linear enclosed mass yields constant vrot, consistent with the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.