density_pos
plain-language theorem explainer
The theorem shows that density at any natural-number rung k equals phi to the power k and is therefore positive. Modelers of neutron-star crusts cite it to guarantee that all five regimes on the phi-ladder carry positive densities. The proof is a direct one-line application of the positivity of powers for a positive base.
Claim. For every natural number $k$, the density at rung $k$ satisfies $0 < phi^k$, where $phi$ is the self-similar fixed point of the Recognition Composition Law.
background
Density is defined as $phi^k$ for natural $k$, placing values on the phi-ladder whose adjacent ratios equal $phi$. The module treats five canonical neutron-star crustal regimes (outer crust, inner crust, nuclear pasta, outer core, inner core) whose densities follow this ladder. Upstream results supply the same positivity claim for energy density in battery-chemistry models and for density rungs in dark-matter halo profiles.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the established fact that the self-similar fixed point phi is positive.
why it matters
It supplies the density_always_pos field required by the neutronStarCert certificate, which also records five regimes and the phi ratio. Parallel certificates in battery chemistry and dark-matter halo profiles reuse the identical positivity statement. The result anchors the positivity requirement inside the phi-ladder construction that follows from the Recognition Composition Law and the forced value of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.