density_pos
plain-language theorem explainer
The theorem asserts that energy density at every natural-number rung on the phi-ladder is strictly positive. Battery-chemistry modelers cite it to confirm that all five canonical families store positive energy. The one-line proof applies the standard lemma on positivity of powers with positive base.
Claim. For every natural number $k$, the energy density $E(k) := phi^k$ satisfies $E(k) > 0$.
background
The module treats battery chemistry as five families (lead-acid, nickel-cadmium, nickel-metal-hydride, lithium-ion, solid-state) whose energy-density ratios follow the phi-ladder. Energy density is the noncomputable definition phi raised to rung index k. This positivity statement is the direct analogue of the density_pos theorems already established for dark-matter halo profiles and neutron-star crustal regimes.
proof idea
One-line wrapper that applies the lemma pow_pos to phi_pos and the exponent k.
why it matters
The result supplies the density_always_pos field inside batteryChemistryCert, which certifies the five chemistries together with the phi-ratio. It mirrors the parallel density_pos declarations in the dark-matter and neutron-star modules. In the Recognition framework it secures the phi-ladder energy formulas (T6 self-similar fixed point) by excluding negative densities from material applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.