density_strictDecr
plain-language theorem explainer
The result shows that density on the phi-ladder decreases strictly with each rung index. Modelers of dark matter halos in the Recognition Science approach cite it when verifying the ordering of the five canonical regimes. The short tactic proof unfolds the density definition, uses the fact that phi exceeds one to establish power growth, and applies the lemma on reciprocals of positive quantities.
Claim. For each natural number $k$, the rung density satisfies $1/phi^{k+1} < 1/phi^k$.
background
The module constructs dark-matter halo profiles from the Recognition Science phi-ladder, placing five regimes at successive rungs with density falling at each step. The rung-density assignment returns the reciprocal of phi raised to the rung index. The upstream result one_lt_phi asserts that phi is strictly greater than one, which is required to obtain strict growth of the powers.
proof idea
Unfold the rung-density assignment to expose the reciprocal powers. Record positivity of phi to the k via pow_pos. Prove phi^k < phi^{k+1} by expanding the successor power and invoking nlinarith together with one_lt_phi. Conclude by applying one_div_lt_one_div_of_lt to the two inequalities.
why it matters
The theorem is invoked inside darkMatterHaloCert to witness the strictly decreasing density property across the five regimes. It thereby supports the claim that the phi-ladder supplies a canonical ordering for NFW, Einasto, and isothermal profiles. Within the broader framework it instantiates the self-similar density scaling expected from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.