vrot_flat_of_linear_Menc
plain-language theorem explainer
Linear enclosed mass growth Menc(r) = α r produces flat rotation curves with constant vrot(r) = sqrt(G α) for every r > 0. Galactic dynamics modelers cite the result when fitting observed flat velocity profiles to linear mass distributions inside the Recognition Science gravity module. The proof substitutes the linear hypothesis into the centripetal velocity expression and cancels algebraically to reach the constant value.
Claim. If the enclosed mass satisfies $M(r) = α r$ for all $r > 0$, then the rotation velocity satisfies $v(r) = √(G α)$ for all $r > 0$.
background
A RotSys is a structure carrying a positive gravitational constant G and a non-negative enclosed-mass function Menc : ℝ → ℝ. The velocity function vrot returns the orbital speed at radius r under Newtonian balance, defined by sqrt(G Menc(r)/r). The lemma lives in the Gravity.Rotation module whose local setting is a rotation system equipped with the RS-native G taken from Constants.G, where G = λ_rec² c³ / (π ℏ).
proof idea
The tactic proof introduces r > 0, substitutes the linear hypothesis to obtain Menc r = α r, then rewrites G Menc r / r to G α by ring simplification followed by field_simp on the nonzero denominator. It finally rewrites the definition of vrot to conclude the equality.
why it matters
The lemma supplies the flat-curve case for linear mass growth, a direct consequence of the centripetal balance inside the Recognition gravity derivations that begin from the J-cost functional equation. It supports rotation-curve modeling that ultimately traces back to the eight-tick octave and D = 3 spatial dimensions fixed by the forcing chain. No downstream theorems are listed, leaving its use open for later galactic-dynamics applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.