g
plain-language theorem explainer
The declaration defines centripetal acceleration g(S, r) for a rotation system S at radius r as the square of rotation velocity divided by r. Researchers modeling galactic dynamics or deriving flat rotation curves within Recognition Science cite it when linking velocity profiles to gravitational acceleration. The definition is a direct one-line algebraic expression built from the vrot function already present in the same module.
Claim. For a rotation system $S$ equipped with gravitational constant $G>0$ and non-negative enclosed-mass function $M_ {enc}$, the centripetal acceleration at radius $r$ is $g(S,r)=v_{rot}(S,r)^2/r$, where $v_{rot}$ denotes the rotation velocity supplied by the system.
background
RotSys is the structure that packages a positive gravitational constant $G$ together with a non-negative function $M_{enc}:ℝ→ℝ$ that returns enclosed mass inside radius $r$. The module Gravity.Rotation works entirely inside this structure, treating rotation velocity $v_{rot}$ as a derived quantity whose square equals $G M_{enc}(r)/r$ for $r>0$. Upstream constants supply the concrete value of $G$ either in RS-native form $G=λ_{rec}^2 c^3/(π ħ)$ or the CODATA numerical value, while the J-cost reparametrization $G(t)=J(e^t)$ supplies the underlying functional-equation origin of the same constant.
proof idea
One-line definition that applies the already-defined vrot function and performs ordinary real division by the radius.
why it matters
The definition supplies the Newtonian centripetal-acceleration expression inside the rotation-system framework, directly enabling the flat-curve identities vrot_flat_of_linear_Menc and g_of_linear_Menc that appear as sibling declarations. It therefore sits at the interface between the universal forcing chain (T5–T8) that fixes $G$ and the concrete gravitational phenomenology required for galactic rotation curves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.