HaloRegime
plain-language theorem explainer
This inductive definition enumerates the five canonical dark matter halo regimes in the Recognition Science framework for galactic density modeling. A physicist fitting rotation curves or halo profiles would cite it to select the appropriate regime at a given radius. The definition proceeds by direct enumeration of the five constructors with automatic derivation of Fintype and equality instances.
Claim. The set of dark matter halo regimes consists of five elements: NFW inner, NFW outer, Einasto profile, isothermal sphere, and truncation edge, each occupying one rung on the $phi$-ladder in density.
background
The module Dark Matter Halo Profile from RS introduces five canonical regimes to realize configDim D = 5. These are the NFW inner regime, NFW outer regime, Einasto profile, isothermal sphere, and truncation edge. Each regime sits one rung down the $phi$-ladder in density, following the Recognition Science derivation from the single functional equation and the Recognition Composition Law.
proof idea
The declaration is an inductive type definition that introduces five constructors corresponding to the regimes. It derives DecidableEq, Repr, BEq, and Fintype automatically to enable cardinality and ordering operations.
why it matters
This definition supplies the domain required by the DarkMatterHaloCert structure, which certifies that the cardinality equals five with positive and strictly decreasing densities. It implements the A6 depth of the Recognition Science framework by enumerating the discrete regimes on the $phi$-ladder. The downstream haloRegime_count theorem confirms the count by direct decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.