vrot_sq
plain-language theorem explainer
Algebraic identity establishing that squared rotation velocity equals gravitational constant times enclosed mass over radius for positive radii in a rotation system. Galaxy modelers deriving flat rotation curves from linear mass growth would cite this when reducing the Newtonian force balance. The proof unfolds the vrot definition then applies the square-root squaring identity after non-negativity checks.
Claim. For a rotation system $S$ with positive gravitational constant $G$ and non-negative enclosed-mass function $M_ {enc}$, and for every radius $r>0$, the squared rotation velocity satisfies $v_{rot}(S,r)^2 = G M_{enc}(r)/r$.
background
A rotation system is the structure containing a positive real $G$ and a function $Menc:ℝ→ℝ$ that returns non-negative values for every radius, together with the positivity witness for $G$. The module treats this structure as the minimal data needed to define rotation velocity via the Newtonian expression $v_{rot}(S,r)=√(G Menc(r)/r)$. Upstream constants supply the explicit RS-native form of $G$ as $λ_{rec}^2 c^3/(π ℏ)$, while the functional-equation reparametrization of $G$ is available but not required for the present algebraic step.
proof idea
The tactic proof first applies dsimp to unfold the definition of vrot into the square-root expression. It then constructs two non-negativity facts: the numerator $G Menc(r)$ is non-negative by positivity of $G$ and the nonnegM field of RotSys, and the full fraction is non-negative by positivity of $r$. The calc block finishes by rewriting with Real.sq_sqrt on the non-negative argument.
why it matters
The lemma supplies the direct algebraic link between enclosed mass and rotation velocity that later siblings use to obtain flat curves when Menc grows linearly. It occupies the Newtonian force-balance step inside the gravity rotation module and inherits the RS-native value of $G$ from the forcing-chain constants. No open scaffolding remains; the identity is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.