nfwProfile
Defines the Navarro-Frenk-White density profile ρ(r) = ρ_s / [(r/r_s)(1 + r/r_s)^2] for Recognition Science models of dark matter halos formed by odd 8-tick ledger shadows. Galaxy dynamics researchers cite it when linking J-cost equilibrium distributions to flat rotation curves. The implementation is a direct algebraic transcription of the standard NFW formula.
claimThe Navarro-Frenk-White halo density profile is given by $ρ(r) = ρ_s / [(r/r_s)(1 + r/r_s)^2]$ for characteristic density $ρ_s$, scale radius $r_s$, and radial coordinate $r$.
background
In Recognition Science, dark matter consists of odd 8-tick phase ledger entries whose spatial distribution minimizes J-cost. The module COS-011 frames this against observed flat galaxy rotation curves, which require extended mass beyond visible baryons. Upstream constants supply the tick as the fundamental time quantum τ₀ = 1 and the phase function kπ/4 for k in Fin 8, while the cost function is the derived cost of a multiplicative recognizer comparator.
proof idea
The definition is a direct one-line algebraic transcription of the standard NFW formula using real division and exponentiation; no lemmas or tactics are invoked.
why it matters in Recognition Science
This definition supplies the cuspy halo form used in subsequent rotation velocity calculations within the module. It connects the ledger shadow mechanism to the core-cusp problem noted in N-body CDM simulations and supports the claim that J-cost equilibrium yields the required 1/r² outer density for flat curves. The placement advances the eight-tick octave and D = 3 framework landmarks by embedding standard astrophysical profiles inside RS-native units.
scope and limits
- Does not derive the NFW form from the Recognition Composition Law or J-uniqueness.
- Does not compute the rotation velocity or velocity dispersion from the density.
- Does not resolve the core-cusp tension with observed galaxy cores.
- Does not incorporate phi-ladder rung scaling or Berry creation thresholds.
formal statement (Lean)
98noncomputable def nfwProfile (rho_s r_s r : ℝ) : ℝ :=
proof body
Definition body.
99 rho_s / ((r / r_s) * (1 + r / r_s)^2)
100
101/-! ## RS: Ledger Shadow Distribution -/
102
103/-- In RS, the dark matter halo is a distribution of ledger shadows:
104
105 Dark matter = odd 8-tick phase ledger entries
106
107 These ledger entries are distributed according to J-cost equilibrium.
108 The J-cost minimum gives the halo density profile. -/