typicalRotationVelocity
plain-language theorem explainer
Recognition Science models flat galaxy rotation curves via ledger shadow distributions. This definition supplies the benchmark Milky Way value of 220 km/s that such models must reproduce at large radii. The assignment is a direct constant definition with no computation or lemmas.
Claim. The typical rotation velocity is the real number 220, expressed in km/s, for the Milky Way galaxy.
background
The module COS-011 sets up galaxy rotation curves in Recognition Science. Stars orbit the galactic center; Newtonian gravity predicts inner solid-body rise followed by Keplerian falloff at large radii. Observed curves instead remain roughly constant from 5 kpc to beyond 30 kpc, requiring 5-10 times the visible mass.
proof idea
The definition is a direct assignment of the constant 220.
why it matters
This value anchors the target for flat rotation curves that the Recognition Science ledger model must explain. It supplies the numerical benchmark for J-cost equilibrium distributions of dark ledger entries. The module connects the constant velocity to the eight-tick octave structure of ledger phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.