module module moderate

`IndisputableMonolith.Cosmology.GalaxyRotation`

GalaxyRotation module assembles definitions for circular velocity and halo profiles in galaxies under Recognition Science. Cosmologists examining flat rotation curves or Tully-Fisher scaling would cite the module for its RS-adapted mass and velocity relations. Content is organized as a collection of definitions and profile constructions that import constants, J-cost, and phi-forcing results.

claimCircular velocity satisfies $v(r) = (G M(r)/r)^{1/2}$ with $M(r)$ the enclosed mass; related objects include isothermal halo, NFW profile, jcost equilibrium profile, MOND acceleration, and Tully-Fisher relation.

background

The module resides in the cosmology domain and imports the RS time quantum tau_0 from Constants, the J-cost ledger structure from Cost, and the self-similarity argument from PhiForcing. PhiForcing shows that phi is forced as the fixed point of a discrete ledger equipped with J-cost. The supplied circular-velocity formula serves as the entry point for applying these structures to galactic dynamics.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the velocity and profile primitives that support downstream results on core-cusp resolution and Tully-Fisher scaling. It links the phi-ladder and J-cost equilibrium to observable galaxy properties, extending the forcing chain into the cosmology domain.

scope and limits

Does not derive rotation curves from first principles without additional assumptions.
Does not address full cosmological structure formation.
Does not provide numerical fits to specific galaxy data.
Does not claim equivalence to standard dark-matter halos outside RS units.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (17)

def circularVelocity L52
theorem keplerian_falloff L59
def typicalRotationVelocity L66
def milkyWayData L72
theorem isothermal_halo L87
def nfwProfile L98
theorem dm_halo_from_ledger L109
theorem jcost_equilibrium_profile L121
def coreCuspProblem L136
theorem rs_predicts_core L148
def mondAcceleration L163
theorem tully_fisher L170
theorem mond_acceleration_phi L183
def btfrData L197
def predictions L209
def summary L226
structure GalaxyRotationFalsifier L240