RotSys
plain-language theorem explainer
RotSys packages a positive gravitational constant with a non-negative enclosed-mass function to serve as the common data structure for rotation-curve calculations. Galaxy-dynamics researchers cite it when they derive centripetal accelerations or flat velocity profiles from linear mass growth. The declaration is a direct structure with four fields and no proof obligations.
Claim. A rotation system consists of a gravitational constant $G>0$ together with an enclosed-mass function $M(r)$ satisfying $M(r)≥0$ for every real radius $r$.
background
Recognition Science obtains the gravitational constant from the functional equation and the phi-ladder; the structure supplies the minimal interface needed to compute Newtonian rotation curves in the Gravity.Rotation module. Upstream results include the RS-native definition of G and the ledger factorization that calibrates the J-cost. The enclosed-mass function is required only to be non-negative; no smoothness or monotonicity is imposed at this level.
proof idea
Direct structure definition. No lemmas or tactics are applied; the four fields are declared explicitly.
why it matters
RotSys is the common interface for every rotation-curve lemma in the module, including vrot, g, and the flat-curve results vrot_flat_of_linear_Menc. It connects the gravitational constant (derived via T5-T8) to observable galactic dynamics and supports the claim that linear mass growth yields flat rotation curves. Downstream results quote it directly when they state algebraic identities such as vrot² = G Menc / r.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.