phi_rung_energy_pos
plain-language theorem explainer
Energy stored at each φ-rung is strictly positive for any integer rung index. Researchers deriving storage density bounds in Recognition Science cite this when establishing the full hierarchy of chemical, nuclear, and mass-energy scales. The proof reduces directly to the product of two positive quantities via the definition of phi_rung_energy.
Claim. For all integers $n$, $0 < E_{coh,storage} · φ^n$, where $E_{coh,storage}$ is the positive coherence energy per recognition event and $φ$ is the golden ratio.
background
In the EnergyStorageDensityStructure module, phi_rung_energy is defined as the product of E_coh_storage and φ raised to the integer rung index n. The module sets energy storage limits from the φ-ladder and J-cost structure, with stored energy given by J(x) times the coherence quantum E_coh = φ^{-5} eV. E_coh_storage_pos supplies the base positivity fact that E_coh_storage itself is a positive power of φ.
proof idea
The term proof unfolds the definition of phi_rung_energy to expose the product E_coh_storage * φ^n, then applies mul_pos to the pair E_coh_storage_pos and zpow_pos phi_pos _.
why it matters
This supplies the positivity conjunct required by rs_energy_storage_hierarchy, which assembles the full chain (positivity, strict increase with rung, and nuclear exceeding chemical). It fills the EN-004.2 slot in the energy storage density derivation, confirming that all φ-rung energies lie above the ground state and supporting the predicted nine-order gap between nuclear and chemical scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.