phonon_rung_strictly_increasing
plain-language theorem explainer
The phonon rung frequencies on the φ-ladder increase strictly with rung index k for any positive base frequency ω₀. Materials physicists screening phonon-mediated superconductors cite this to confirm the discrete spectrum is ordered by construction. The proof is a one-line wrapper that rewrites the successor definition, invokes positivity of the current rung together with φ > 1, and closes via non-linear arithmetic.
Claim. For any real number ω₀ > 0 and natural number k, the frequency at rung k satisfies ω₀ φ^k < ω₀ φ^{k+1}.
background
The module supplies the φ-ladder structure for phonon frequencies in materials, where resonance for superconductivity requires ω_p = ω₀ φ^k for integer k. The rung function maps base frequency and index to the corresponding ladder value, with successor defined by multiplication by φ. Upstream, the lemma one_lt_phi states 1 < φ and the positivity result for rungs establishes that every rung frequency remains positive when ω₀ > 0. This ordering property sits inside the Recognition Science setting of discrete φ-tiers for physical quantities.
proof idea
The proof rewrites the target inequality using the successor definition of the rung function. It then applies the positivity lemma for the rung at k and the lemma that φ exceeds one. Non-linear arithmetic finishes the argument directly from these two facts.
why it matters
The result is referenced inside the master certificate phiLadderPhononResonanceCert that bundles positivity, successor, strict increase, and adjacent ratio to certify the full ladder model. It supplies the ordering step required by the RS_PAT_008–RS_PAT_010 chain for superconductivity screening and hydride optimization. The ordering is consistent with the self-similar fixed point φ forced in the T0–T8 chain and with the discrete spectrum used throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.