nfwProfile
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.