IndisputableMonolith.Physics.DarkMatterHaloProfileFromRS
Defines the Recognition Science dark-matter halo density on the phi-ladder: discrete halo regimes, a rung-indexed density map, and a certificate of positivity plus strict radial decrease. Astrophysicists matching RS predictions to rotation curves or lensing would cite the density rung and DarkMatterHaloCert. The module is largely definitional, with short positivity and monotonicity lemmas packaging the profile.
claimThe module introduces a finite halo-regime type, a density $\rho$ indexed by $\varphi$-ladder rungs, proofs that $\rho>0$ and that $\rho$ is strictly decreasing in the rung index, and a certificate bundle packaging those facts for downstream use.
background
Recognition Science places masses and field scales on a discrete $\varphi$-ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Dark-matter halos are treated the same way: radial density is assigned by rung rather than by a continuous NFW-style ansatz.
The module lives in the Physics domain and imports only Mathlib and RS Constants (including the fundamental tick $\tau_0$). Sibling names mark the local vocabulary: HaloRegime (finite regime classification), densityRung (rung-to-density map), density_pos and density_strictDecr (sign and monotonicity), and DarkMatterHaloCert / darkMatterHaloCert (the packaged certificate).
proof idea
This is primarily a definition module. HaloRegime and densityRung introduce the discrete profile; density_pos and density_strictDecr are short positivity and strict-decrease arguments on that map; DarkMatterHaloCert bundles the resulting properties into one certificate object witnessed by darkMatterHaloCert.
why it matters in Recognition Science
Supplies the RS-native dark-matter halo profile for later comparison with galactic rotation curves and lensing. No downstream consumers are recorded yet in the mirror graph. It ties the $\varphi$-ladder mass formula and the forcing-chain landmarks (T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) to an astrophysical observable: the radial density falloff of a dark halo. The certificate pattern matches other RS Physics certs that package positivity and monotonicity for higher-level claims.
scope and limits
- Does not derive NFW or Einasto profiles from first principles.
- Does not fit observational rotation-curve or lensing data.
- Does not prove uniqueness of this density among all RS-compatible profiles.
- Does not model baryonic feedback or multi-component halos.
- Does not compute numerical halo masses or concentration parameters.