pith. sign in
module module high

IndisputableMonolith.Cosmology.GalaxyRotation

show as:
view Lean formalization →

The Cosmology.GalaxyRotation module supplies definitions for circular velocity profiles and related rotation-curve objects under the Recognition Science ledger. Researchers modeling galactic dynamics or testing alternatives to dark-matter halos would cite these objects when comparing RS-native predictions to observed curves. The module is definitional, importing the J-cost structure and the phi-forcing result to express velocity via the enclosed-mass formula in RS units.

claimThe circular velocity at radius $r$ is $v(r)=\sqrt{G M(r)/r}$, where $M(r)$ is the enclosed mass obtained from the phi-ladder.

background

The module resides in the cosmology domain and imports Constants (defining the RS time quantum $ au_0=1$ tick), Cost (supplying the J-cost functional), and PhiForcing. The upstream PhiForcing module proves that $\phi$ is forced by self-similarity in a discrete ledger with J-cost. These imports allow the circular-velocity expression to be written in RS-native units where $c=1$, $G=\phi^5/\pi$, and masses lie on the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the velocity and halo-profile objects used by sibling declarations such as tully_fisher, mondAcceleration, and rs_predicts_core. It thereby extends the Recognition Composition Law and the eight-tick octave to galactic scales, linking the T5 J-uniqueness and T8 D=3 results to observable rotation curves.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)