Cosmology Galaxy Rotation Keplerian Falloff

Keplerian falloff

In classical physics, a star orbiting a point mass M at distance r feels gravity that weakens with the square of distance. The orbital speed that balances this gravity is v = √(GM/r), so v falls off as 1/√r. This is the Keplerian falloff: double the distance and the speed drops by about 29 percent. Astronomers use this as the baseline expectation for stars in the outer parts of a galaxy, where most of the visible mass lies concentrated near the center.

For the Milky Way, the baseline predicts a solar orbital speed of about 220 km/s at the Sun's position, falling to roughly 150 km/s at 20 kpc from the center. Observations instead show the speed staying near 220 km/s out to that distance and beyond. This mismatch, the flat rotation curve problem, is one of the main pieces of evidence for dark matter. The standard fix assumes a dark matter halo with density falling as 1/r² at large radius, which produces a constant orbital speed.

In Recognition Science, the declaration keplerian_falloff states the classical baseline: v ∝ 1/√r for a point mass. The declaration's proof is the trivial proof of the proposition True, and the module that contains it is explicitly labeled a sketch module. This means the declaration establishes the classical formula, nothing more. It does not claim that real galaxies follow this falloff, does not derive the flat rotation curve, and does not introduce any Recognition Science mechanism for dark matter. Those targets belong to other declarations in the same module, all of which are also sketches concluding in True.

The distinction matters because the module also records intentions: dark matter as ledger shadows, halos from J-cost equilibrium, flat curves from 1/r² density. Those are stated as targets, not as results. The keplerian_falloff declaration sits at the classical starting point, the baseline that observations contradict. A reader who wants the Recognition Science account of the flat curve itself must look to the sketch targets, not to this declaration.

/-- For a point mass (or spherical distribution):
    v(r) ∝ 1/√r (Keplerian falloff)

    But observed: v(r) ≈ constant! -/
theorem keplerian_falloff :
    -- v ∝ 1/√r for point mass
    True := trivial

/-- For a point mass (or spherical distribution):
    v(r) ∝ 1/√r (Keplerian falloff)

    But observed: v(r) ≈ constant! -/
theorem keplerian_falloff :
    -- v ∝ 1/√r for point mass
    True := trivial

What this page does not claim

The declaration does not claim that real galaxies follow Keplerian falloff. The declaration does not derive the flat rotation curve or any dark matter mechanism. The declaration does not establish the Recognition Science account of galaxy rotation; that remains a sketch target.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/GalaxyRotation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: