typicalRotationVelocity
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the velocity from ledger parameters or J-cost minimization.
- Does not specify the radial profile or halo density law.
- Does not address rotation curves of galaxies other than the Milky Way.
- Does not incorporate phi-ladder mass scaling or alpha-band constraints.
formal statement (Lean)
66noncomputable def typicalRotationVelocity : ℝ := 220 -- km/s (Milky Way)
proof body
Definition body.
67
68/-- The Milky Way rotation curve:
69 - Sun at 8 kpc: v ≈ 220 km/s
70 - Outer disk at 20 kpc: v ≈ 220 km/s (still flat!)
71 - Visible mass would give v ≈ 150 km/s at 20 kpc -/