density_pos
plain-language theorem explainer
The theorem shows that densityRung k remains strictly positive for every natural number k. Dark-matter halo modelers and Recognition Science certifiers cite it when verifying the five phi-ladder regimes. The proof is a one-line term that unfolds the definition and applies the standard positivity lemmas for division and exponentiation.
Claim. For every natural number $k$, the density at phi-ladder rung $k$ satisfies $1/phi^k > 0$, where $phi$ is the self-similar fixed point.
background
The module places five canonical dark-matter halo regimes on the phi-ladder, each one rung lower in density. densityRung is the auxiliary definition densityRung k := 1 / phi^k. Parallel positivity statements appear in BatteryChemistryFromPhiLadder.density_pos and NeutronStarCrustalRegimesFromRS.density_pos, both proved by the same pow_pos phi_pos k tactic.
proof idea
The term proof first unfolds densityRung to expose the division 1 / phi^k, then supplies the exact term div_pos one_pos (pow_pos phi_pos k). It therefore inherits the upstream facts that phi > 0 and that positive bases raised to natural powers stay positive.
why it matters
density_pos supplies the density_always_pos field inside darkMatterHaloCert, which certifies the five halo regimes together with the count and strict-decrease properties. The same pattern appears in batteryChemistryCert and neutronStarCert. It therefore anchors the positivity requirement for all phi-ladder densities used in the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.