Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.GalaxyRotation

show as:
view Lean formalization →

Galaxy rotation curves under Recognition Science: circular velocity from enclosed mass, comparison of Keplerian falloff with isothermal and NFW halos, and an RS ledger-derived halo tied to J-cost equilibrium. Cosmologists comparing dark-matter profiles, MOND, and the Tully–Fisher relation to RS predictions would cite it. The module is mostly definitions and named profile identities, with φ-forcing and cost structure imported rather than reproved.

claimAt radius $r$, circular speed is $v(r)=\sqrt{G M(r)/r}$. The module records Keplerian falloff, isothermal and NFW halo profiles, a ledger-derived dark-matter halo, a $J$-cost equilibrium density, the core–cusp tension, an RS core prediction, MOND acceleration $a_{\mathrm{MOND}}$, and the Tully–Fisher scaling, all in RS-native constants ($G=\varphi^5/\pi$, etc.).

background

Recognition Science fixes $G$ and related constants from the forced golden ratio $\varphi$ (PhiForcing: self-similar discrete ledger with $J$-cost) and the cost calculus in Cost. In RS-native units $c=1$ and $G=\varphi^5/\pi$. Galaxy dynamics then reduce to how enclosed mass $M(r)$ sets circular speed.

Classical baselines appear as named objects: Keplerian $v\propto r^{-1/2}$ for concentrated mass, isothermal halo (flat $v$), and the NFW cusp. The RS side replaces ad hoc halo parameters by a ledger-derived density and a $J$-cost equilibrium profile. The core–cusp problem is the observational preference for cored centers versus NFW cusps; the module states an RS claim that the ledger favors cores.

MOND acceleration and the Tully–Fisher relation sit as comparison targets: empirical scalings any RS halo story must match or reinterpret.

proof idea

Definition-and-comparison module, not a single end-to-end theorem. It introduces circular velocity from $v^2=GM(r)/r$, records Keplerian falloff, and names standard halo shapes (isothermal, NFW) beside RS constructions (halo from ledger, $J$-cost equilibrium). Core–cusp and "RS predicts core" are stated as problem/claim interfaces against those profiles. MOND acceleration and Tully–Fisher appear as reference relations. Heavy lifting on $\varphi$ and $J$ is imported from PhiForcing and Cost; local content is packaging and identity-level statements.

why it matters in Recognition Science

Places galaxy-scale dynamics inside the RS constant and cost stack: once $G$ and $\varphi$ are forced, rotation curves become a test of whether ledger mass distributions reproduce flat curves, cores, and Tully–Fisher without a separate dark-matter field. Downstream use is not yet wired in-repo (no used_by edges); the natural parents are cosmology and phenomenology layers that quote RS halo predictions against SPARC-style data. Ties to framework landmarks via $\varphi$-forced $G$ and $J$-cost equilibrium rather than new forcing-chain steps (T5–T8 stay upstream). Open surface: discharging core prediction and ledger-halo matches as proved theorems rather than named interfaces.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)