circularVelocity
plain-language theorem explainer
The definition supplies the Newtonian circular velocity v(r) = sqrt(G M / r) for a star at radius r with enclosed mass M. Galaxy modelers in the Recognition Science framework cite it when contrasting Keplerian falloff against observed flat curves from ledger distributions. The implementation is a direct one-line expression using the RS-derived gravitational constant.
Claim. The circular velocity at radius $r > 0$ for enclosed mass $M$ is given by $v(r) = √(G M / r)$, where $G$ is the Recognition Science gravitational constant.
background
The module COS-011 derives galaxy rotation curves from dark matter ledger distribution in Recognition Science. Dark matter consists of ledger shadows from odd 8-tick phases, with the halo formed by a distribution of dark ledger entries that produces J-cost equilibrium and flat rotation. Upstream, G is the RS-native constant defined as lambda_rec² c³ / (π ħ) in Constants, with an alternative CODATA numerical form also available.
proof idea
One-line wrapper that computes the square root of the product of the gravitational constant G and the enclosed mass M divided by the radius r.
why it matters
This definition anchors the Newtonian baseline inside COS-011, enabling the contrast with flat curves produced by J-cost equilibrium profiles. It feeds sibling constructions such as keplerian_falloff and typicalRotationVelocity while connecting to the eight-tick octave and phi-ladder structure that governs dark-matter halos. The placement prepares the module for later ledger-based derivations of mondAcceleration and tully_fisher relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.