Cosmology Galaxy Rotation

Galaxy rotation curves

Galaxy rotation curves plot the orbital speed of stars and gas against their distance from a galaxy's center. For the solar system, Kepler's laws govern the motion: inner planets move faster, and the speed falls off as the inverse square root of distance. Astronomers expected the same pattern in galaxies, with the visible stars and gas providing the gravitational pull. Observations from the 1970s onward, especially those by Vera Rubin, showed something else: the rotation curve stays roughly flat far beyond the visible disk. Outer stars orbit just as fast as inner ones, implying far more mass than telescopes can see. This discrepancy, often stated as a factor of five to ten times the visible mass, is the flat rotation curve problem.

The standard cosmological solution places each galaxy inside a dark matter halo, a roughly spherical cloud of unseen matter that extends well past the visible stars. If the halo's density falls off as one over radius squared, ρ ∝ 1/r², then the orbital speed becomes constant at large radius, matching the flat curves. The Milky Way offers a concrete example: at the solar radius of 8 kiloparsecs the rotation speed is about 220 km/s, and at 20 kiloparsecs it is still about 220 km/s, whereas the visible matter alone would predict only about 150 km/s. This is a measured discrepancy, not a theoretical one.

In Recognition Science, the framework models dark matter as ledger shadows, entries in a discrete record of recognition events that occupy odd phases of an eight-tick cycle. The dark matter halo becomes an equilibrium distribution of these dark ledger entries, and the flat rotation curve follows from a J-cost equilibrium, the same cost function that the framework's core theorems force. The module in the machine-checked library of formal theorems states this as a target, not a result: the declaration jcost_equilibrium_profile is a sketch whose conclusion is the tautology True, and the docstring explicitly warns that nothing in the module is established. The framework also records predictions: cores rather than cusps at galaxy centers, a Tully-Fisher relation where baryonic mass scales as the fourth power of rotation speed, and a MOND-like acceleration scale near 1.2e-10 m/s², possibly related to the golden ratio ladder. These are stated as intentions, not as derived theorems.

What the module does establish in plain language is a falsifier structure. It names three conditions that would refute the account: rotation curves that are not flat, a MOND-like theory that works everywhere with no need for dark matter, or a mismatch between the ledger distribution and observed galaxy properties. This is a hypothesis with a named falsifier, which is the honest status of the whole galaxy rotation program in the framework. The classical dark matter explanation remains the standard one, and the Recognition Science account is a proposed alternative that has not yet been formalized into a proved theorem.

/-- The Milky Way rotation curve:
    - Sun at 8 kpc: v ≈ 220 km/s
    - Outer disk at 20 kpc: v ≈ 220 km/s (still flat!)
    - Visible mass would give v ≈ 150 km/s at 20 kpc -/
def milkyWayData : List (String × String) := [
  ("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")
]

/-- To get v = constant, we need M(r) ∝ r:
    v² = G M(r) / r
    v = constant → M(r) ∝ r

    This requires ρ(r) ∝ 1/r²:
    M(r) = ∫ 4πr² ρ(r) dr = ∫ 4πr² × (ρ₀/r²) dr = 4πρ₀ r -/
theorem isothermal_halo :
    -- ρ ∝ 1/r² gives flat rotation curve
    True := trivial

/-- In RS, the dark matter halo is a distribution of ledger shadows:

    Dark matter = odd 8-tick phase ledger entries

    These ledger entries are distributed according to J-cost equilibrium.
    The J-cost minimum gives the halo density profile. -/
theorem dm_halo_from_ledger :
    -- DM halo = equilibrium distribution of ledger shadows
    True := trivial

/-- The J-cost equilibrium condition:

    For a self-gravitating system:
    ∇J = 0 at equilibrium

    This gives the density profile.
    For spherical symmetry with isothermal J-cost:
    ρ ∝ 1/r² (isothermal sphere) -/
theorem jcost_equilibrium_profile :
    -- J-cost equilibrium → ρ ∝ 1/r² at large r
    True := trivial

What this page does not claim

The Recognition Science account of flat rotation curves is proved; the module explicitly marks it as a sketch. The framework derives the dark matter density profile from first principles; the 1/r² form is assumed from the standard halo model. The MOND acceleration scale is derived; the module only notes a possible relation to the golden ratio ladder.

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: