g
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not define or compute the enclosed-mass function Menc.
- Does not enforce r>0 or positivity of vrot.
- Does not derive the explicit form of vrot from first principles.
- Does not address non-circular orbits or relativistic corrections.
formal statement (Lean)
19noncomputable def g (S : RotSys) (r : ℝ) : ℝ :=
proof body
Definition body.
20 (vrot S r) ^ 2 / r
21
22/-- Algebraic identity: `vrot^2 = G Menc / r` for `r > 0`. -/