vrot_flat_of_linear_Menc_Newtonian
plain-language theorem explainer
The lemma shows that a linear enclosed-mass profile Menc(r) = γ r with γ nonnegative yields a constant Newtonian rotation velocity sqrt(G γ) at every radius r > 0. Galaxy dynamicists modeling flat rotation curves from linear mass growth would cite the result when working in the Newtonian limit. The proof is a direct algebraic reduction: substitute the mass hypothesis into the vrot definition, simplify the radicand via field tactics, and conclude.
Claim. Let S be a rotation system with gravitational constant G > 0 and enclosed-mass function Menc. For any γ ≥ 0, if Menc(r) = γ r holds for all r > 0, then the rotation velocity satisfies vrot(S, r) = √(G γ) for all r > 0.
background
A rotation system is a structure carrying a positive real G, a nonnegative function Menc : ℝ → ℝ, and the derived velocity vrot(S, r) := √(G · Menc(r) / r). The module works entirely in this Newtonian setting. Upstream constants supply G in RS-native form λ_rec² c³ / (π ħ) and the CODATA value, but the lemma treats G as an arbitrary positive parameter.
proof idea
The tactic proof introduces r > 0, applies the linear-mass hypothesis to replace Menc(r), confirms G γ ≥ 0, then rewrites the fraction G Menc(r)/r by substitution and field_simp to obtain G γ. It finishes by dsimp on vrot followed by a single rewrite of the simplified radicand.
why it matters
The result supplies the Newtonian benchmark for flat rotation curves under linear mass growth inside the Recognition Science gravity module. It closes the classical case before any J-cost or ILG corrections are applied, consistent with the framework's separation of Newtonian and Recognition-derived regimes. No downstream theorems are recorded, indicating it functions as a terminal Newtonian reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.