Cosmology Galaxy Rotation Isothermal Halo

Isothermal halo

An isothermal halo is a model of dark matter distribution in a galaxy, named for its resemblance to the density profile of a self-gravitating ideal gas at constant temperature. The defining property is that the mass density ρ falls off as the inverse square of the distance r from the galactic center: ρ ∝ 1/r². This is not a prediction of any fundamental theory but a working assumption used in astronomy because it has a simple consequence: it makes the orbital speed of stars and gas nearly constant at large radii, matching the observed flat rotation curves of spiral galaxies.

The classical picture of galaxy rotation begins with a point mass, for which Newtonian gravity gives a Keplerian falloff, v ∝ 1/√r, and with solid-body rotation, v ∝ r, for the inner disk. Observations of the Milky Way and other spirals show neither: the rotation velocity stays near 220 km/s from the solar neighborhood out to 20 kiloparsecs, while the visible matter alone would predict about 150 km/s at the outer radius. The standard resolution is to embed the galaxy in a dark matter halo; the isothermal profile is the simplest form that reproduces the flat curve.

In Recognition Science, the isothermal halo is not claimed as a derived result. The declaration named isothermal_halo in the framework's machine-checked library is a sketch module: its statement concludes in the trivial proposition True, meaning it records an intention to establish that ρ ∝ 1/r² gives a flat rotation curve, not the establishment itself. The framework models dark matter as ledger shadows, discrete records of recognition events in odd phases of an eight-tick cycle, and proposes that the halo is the equilibrium distribution of such entries. That proposal is a definitional model, not a theorem.

The framework's library also contains a falsifier structure: a named set of conditions under which the recognition account would fail, such as rotation curves that are not flat or a modified gravity theory that works everywhere without dark matter. This is a hypothesis with a specified test, not a proof. The library's summary list states the intended claims, including flat curves from ρ ∝ 1/r² and a Tully-Fisher relation, but these are targets for future formalization, not established results.

/-- 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

/-- 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 derivation would be falsified if:
    1. Rotation curves not flat (already confirmed)
    2. No dark matter (MOND works everywhere)
    3. Ledger distribution doesn't match observations -/
structure GalaxyRotationFalsifier where
  curves_not_flat : Prop
  mond_works_everywhere : Prop
  ledger_mismatch : Prop
  falsified : curves_not_flat ∨ mond_works_everywhere → False

What this page does not claim

The isothermal halo profile is not proved by the framework; the declaration is a sketch whose statement is trivially true. The framework does not claim that dark matter consists of physical ledger entries, only that it models it that way. No claim is made that the framework's predictions, such as cores or the Tully-Fisher relation, have been verified against data.

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: