g_of_linear_Menc
plain-language theorem explainer
Under linear enclosed mass growth Menc(r) = α r the centripetal acceleration satisfies g(r) = (G α)/r for r > 0. Galaxy rotation-curve modelers cite the result when deriving constant orbital speeds from a simple mass profile. The proof substitutes the linear hypothesis into the vrot definition, simplifies the squared term with ring and field_simp, confirms non-negativity via nonnegM and posG, then back-substitutes into the g definition.
Claim. Let S be a rotation system with positive gravitational constant G and non-negative enclosed-mass function Menc. If Menc(r) = α r for every r > 0, then the centripetal acceleration obeys g(S, r) = (G α)/r for every r > 0.
background
A rotation system is a structure carrying a positive real G together with a function Menc : ℝ → ℝ that returns non-negative values for every radius. The rotation velocity is obtained by taking the positive square root of G Menc(r)/r, and the centripetal acceleration is defined as that velocity squared divided by r. The lemma sits inside the Newtonian rotation module whose only import is Mathlib; it draws the concrete value of G from the upstream Constants module where G is expressed as λ_rec² c³/(π ħ).
proof idea
The tactic proof opens by fixing r > 0 and instantiating the linear-mass hypothesis. It rewrites G Menc(r)/r to G α via ring and field_simp, verifies the radicand is non-negative by multiplying posG with nonnegM and dividing by r, applies Real.sq_sqrt, then substitutes the resulting constant into the definition of g to obtain the target expression.
why it matters
The lemma supplies the algebraic step needed to obtain flat rotation curves once linear mass growth is assumed, thereby linking the Newtonian gravity layer to the Recognition Science mass-ladder construction. It sits downstream of the G definition in Constants and upstream of any later flat-curve corollaries in the same module. No used-by edges are recorded yet, leaving open the question of how the result composes with the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.