pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Cosmology.GalaxyRotation

show as:
view Lean formalization →

The GalaxyRotation module supplies circular velocity and supporting galaxy profile definitions in the Recognition Science framework. It equips cosmologists studying rotation curves and dark-matter alternatives with RS-adapted expressions for halos and relations such as Tully-Fisher. The module is definitional, importing constants, cost structure, and phi-forcing to set up the ledger-based mass distributions.

claim$v(r) = √(G M(r)/r)$ with $M(r)$ the enclosed mass, together with isothermal halo, NFW profile, jcost equilibrium profile, MOND acceleration, and Tully-Fisher relation derived from the phi-ladder.

background

Recognition Science builds dynamics from a discrete ledger carrying J-cost, with J(x) = (x + x^{-1})/2 - 1 and phi forced as the self-similar fixed point. The GalaxyRotation module applies this setting to galactic scales by defining mass profiles and velocities that inherit the eight-tick octave and D = 3 from the upstream forcing chain. Constants supplies the native time quantum τ₀ = 1 tick while PhiForcing establishes the self-similarity that fixes phi and therefore the mass-ladder spacing used for halo models.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete expressions that link the J-cost ledger to observable galactic dynamics, feeding downstream results on core-cusp resolution and the Tully-Fisher relation. It closes the step from the fundamental phi-forcing theorem to cosmology-scale predictions without introducing new hypotheses.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)