densityRung
plain-language theorem explainer
densityRung supplies the explicit density value at rung k on the phi-ladder as the reciprocal of phi to the power k. Dark matter halo modelers working in Recognition Science cite it when fixing the discrete density steps for the five canonical regimes. The assignment is a direct definition with no reduction or lemmas required.
Claim. The density at rung $k$ on the phi-ladder is given by $1/phi^k$ for each natural number $k$.
background
Recognition Science organizes densities on the phi-ladder, where successive rungs scale by the inverse of phi, the self-similar fixed point forced in T6 of the UnifiedForcingChain. The module DarkMatterHaloProfileFromRS places five halo regimes (NFW inner, NFW outer, Einasto, isothermal sphere, truncation edge) at successive rungs, each one step down in density, with configDim D = 5. Phi is imported from Constants and satisfies the positivity and growth properties used by dependent results.
proof idea
This is a direct definition that assigns 1 / phi ^ k to densityRung k. No lemmas or tactics are applied; the expression serves as the base for unfolding in the positivity and strict decrease theorems of the same module.
why it matters
This definition supplies the density values required by DarkMatterHaloCert to certify five regimes with always-positive and strictly decreasing densities. It realizes the rung structure for the phi-ladder in the halo profile derivation, aligning with the Recognition Science use of discrete phi-scaling for physical quantities. It closes the basic density assignment for the A6 depth module with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.