darkMatterHaloCert
plain-language theorem explainer
darkMatterHaloCert constructs the certificate asserting five dark-matter halo regimes with positive and strictly decreasing densities on the phi-ladder. Galaxy modelers working in Recognition Science would cite it to confirm the NFW-Einasto-isothermal sequence satisfies the required monotonicity. The construction is a direct record instantiation that assigns the pre-proved lemmas haloRegime_count, density_pos, and density_strictDecr to the three structure fields.
Claim. Let HaloRegime be the finite type of five canonical halo regimes and let densityRung(k) be the density at rung k on the phi-ladder. The certificate asserts that card(HaloRegime) = 5, densityRung(k) > 0 for every natural number k, and densityRung(k+1) < densityRung(k) for every k.
background
The module treats dark-matter halos at A6 depth by placing five regimes (NFW inner, NFW outer, Einasto profile, isothermal sphere, truncation edge) one rung apart on the phi-ladder, each with density decreasing by the factor phi. DarkMatterHaloCert is the structure that packages the three required properties: exact cardinality five, universal positivity, and strict monotonic decrease of densityRung. Upstream, haloRegime_count proves the cardinality by decision; density_pos and density_strictDecr unfold densityRung and apply the positivity and growth lemmas for phi that originate in BatteryChemistryFromPhiLadder.density_pos.
proof idea
The definition is a one-line wrapper that constructs the DarkMatterHaloCert record by direct field assignment: five_regimes receives haloRegime_count, density_always_pos receives density_pos, and density_strictly_decreasing receives density_strictDecr. No further tactics or reductions are performed.
why it matters
This definition closes the certification of the five-regime halo profile inside the A6 module, ensuring the density properties required by the Recognition Science phi-ladder are formally recorded. It sits downstream of the regime-count and density lemmas and supplies the interface that later halo-dynamics or rotation-curve results would invoke. The construction aligns with the framework's derivation of spatial structure from the eight-tick octave and the self-similar fixed point phi, though no immediate parent theorem or open question is recorded in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.