higher_rung_denser
plain-language theorem explainer
Higher rungs on the phi-ladder produce strictly larger energy storage density ratios than lower ones. Researchers modeling RS-derived storage hierarchies cite this result when ordering mechanical, chemical, and nuclear scales. The proof is a direct reduction that unfolds the ratio definition to a positive power of phi and invokes the established inequality 1 < phi together with omega to confirm the exponent sign.
Claim. Let $n, m$ be integers satisfying $m < n$. Then the energy storage density ratio between rung $n$ and rung $m$ exceeds 1, where the ratio equals the golden ratio raised to the power $n-m$.
background
The EN-004 module derives fundamental limits on energy storage per unit mass or volume from the phi-ladder and J-cost structure. Energy takes the form $E = J(x) · E_{coh}$ with coherence quantum $E_{coh} = phi^{-5}$ eV; the cost function is $J(x) = ½(x + x^{-1}) - 1$, which vanishes at the ground state $x=1$ and diverges at the extremes. Storage density ratios between rungs are defined directly as $phi^{n-m}$ (EN-004.12).
proof idea
The term proof first unfolds the definition of storage_density_ratio, reducing the claim to $1 < phi^{n-m}$. It then applies one_lt_zpow₀ to the upstream fact one_lt_phi (1 < phi) while omega confirms that the exponent $n-m$ is positive from the hypothesis $m < n$.
why it matters
This result (EN-004.13) supplies the strict monotonicity of storage density with rung height and feeds the EN-004 certificate, which records the full hierarchy mechanical < chemical < nuclear. It realizes the module claim that consecutive phi-rungs differ by the factor phi and supports the predicted nuclear-to-chemical ratio of order $phi^{45}$. The theorem closes the density-ordering step in the phi-ladder energy hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.