phi_ladder_energy_strictly_increasing
plain-language theorem explainer
The energy stored on successive rungs of the φ-ladder increases strictly with rung index. Engineers and physicists deriving recognition-based bounds on chemical versus nuclear storage scales would cite this monotonicity to separate the hierarchies. The short term proof reduces the inequality to the positivity of the coherence energy together with the strict growth of positive powers of φ under the given integer ordering.
Claim. Let $E(n) = E_0 · φ^n$ denote the energy stored on rung $n$ of the φ-ladder, where $E_0 > 0$ is the coherence energy per recognition event and $φ > 1$ is the golden ratio. Then $n < m$ implies $E(n) < E(m)$.
background
In the EN-004 module energy storage is constructed from the φ-ladder: each integer rung $n$ stores energy $E_0 · φ^n$, where $E_0$ is the positive coherence quantum $E_{coh storage}$. The positivity of this base energy follows from the theorem that unfolds the definition to a positive power of φ. The golden ratio satisfies $1 < φ$ by the lemma one_lt_phi imported from Constants and PhiSupport. The local theoretical setting derives practical storage limits from the J-cost function, with chemical and nuclear scales separated by integer powers of φ.
proof idea
The proof is a one-line wrapper. It unfolds the definition of rung energy to expose the product of the positive coherence energy with φ raised to the rung index, applies the left-multiplication inequality for positive factors, and closes with the zpow monotonicity lemma using $1 < φ$ and the hypothesis $n < m$.
why it matters
This monotonicity is invoked inside rs_energy_storage_hierarchy to obtain the three-scale energy ordering (chemical < nuclear < mass-energy) and is listed as a verified component in the en004_certificate. It supplies the missing step that higher rungs on the φ-ladder always yield strictly larger energies, aligning with the Recognition Science claim that storage scales are quantized on the ladder and separated by factors of φ. No open scaffolding questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.