vrot_sq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume any specific growth law for Menc beyond non-negativity.
- Does not incorporate relativistic or post-Newtonian corrections.
- Does not evaluate numerical values of G or produce sample rotation curves.
- Does not address orbital stability or time-dependent dynamics.
formal statement (Lean)
23lemma vrot_sq (S : RotSys) {r : ℝ} (hr : 0 < r) :
24 (vrot S r) ^ 2 = S.G * S.Menc r / r := by
proof body
Tactic-mode proof.
25 dsimp [vrot]
26 have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
27 have hM : 0 ≤ S.Menc r := S.nonnegM r
28 exact mul_nonneg (le_of_lt S.posG) hM
29 have hfrac_nonneg : 0 ≤ S.G * S.Menc r / r := by
30 exact div_nonneg hnum_nonneg (le_of_lt hr)
31 calc
32 (Real.sqrt (S.G * S.Menc r / r)) ^ 2 = S.G * S.Menc r / r := by
33 rw [Real.sq_sqrt hfrac_nonneg]
34
35/-- If the enclosed mass grows linearly, `Menc(r) = α r` with `α ≥ 0`, then the rotation curve is flat:
36 `vrot(r) = √(G α)` for all `r > 0`. -/