milkyWayData
plain-language theorem explainer
The definition supplies four observational benchmarks for the Milky Way rotation curve: solar radius 8 kpc at 220 km/s, outer disk 20 kpc still at 220 km/s, visible-mass prediction of 150 km/s at 20 kpc, and a factor-of-two mass deficit. Cosmologists modeling flat curves or Recognition Science ledger halos reference these points as input. It is a static list definition with no computation or lemmas.
Claim. Milky Way rotation data is the list of pairs: (``Solar radius'', ``8 kpc, v ≈ 220 km/s''), (``Outer disk'', ``20 kpc, v ≈ 220 km/s''), (``Expected from visible'', ``v ≈ 150 km/s at 20 kpc''), (``Missing mass'', ``Factor of ~2 at 20 kpc'').
background
Module COS-011 frames galaxy rotation curves within Recognition Science by contrasting Keplerian falloff with observed flat curves that require 5-10 times more mass. Dark matter appears as ledger shadows from odd 8-tick phases whose J-cost equilibrium distribution yields ρ ∝ 1/r² and constant v. Upstream results supply G = λ_rec² c³ / (π ℏ) from Constants and ledger factorization structures from DAlembert.LedgerFactorization.
proof idea
The definition is a direct list literal embedding four string pairs. No lemmas or tactics are invoked; it functions as hardcoded observational input for sibling functions such as circularVelocity and nfwProfile.
why it matters
The data anchors the COS-011 claim that ledger shadows produce flat curves via J-cost equilibrium on the phi-ladder. It supplies the concrete benchmarks that downstream siblings (nfwProfile, mondAcceleration, tully_fisher) use to contrast standard halos with RS predictions. The entry closes the observational gap between T7 eight-tick structure and D=3 spatial halo profiles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.