haloRegime_count
plain-language theorem explainer
The declaration establishes that the inductive type enumerating canonical dark-matter halo regimes has cardinality exactly five. Researchers deriving RS-based halo density profiles would cite this when assembling certification data. The proof is a one-line wrapper that invokes the decide tactic on the decidable equality supplied by the inductive definition.
Claim. The finite type of dark-matter halo regimes has cardinality five: $|HaloRegime| = 5$.
background
The module Dark Matter Halo Profile from RS defines five canonical regimes that realize configDim D = 5. The inductive type HaloRegime enumerates them as nfwInner, nfwOuter, einasto, isothermal, and truncation; each sits one rung down the phi-ladder in density. The upstream result is precisely this inductive definition, which automatically derives DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality of the finite type HaloRegime.
why it matters
This supplies the five_regimes field inside the downstream darkMatterHaloCert definition that bundles the full halo-profile certification. It directly realizes the A6-depth claim of five regimes in the Recognition Science framework and connects to the phi-ladder structure and configDim D = 5. No open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.