phi_rpow_le_of_le
plain-language theorem explainer
Golden ratio powers preserve order on the reals: if y ≤ z then φ^y ≤ φ^z. Numerics code that builds interval bounds for the phi-ladder cites the result when propagating inequalities through exponentiation. The term proof is a direct one-line application of the monotonicity lemma for the map x ↦ φ^x.
Claim. For the golden ratio $φ > 1$ and real numbers $y ≤ z$, one has $φ^y ≤ φ^z$.
background
The lemma sits inside the Numerics.Interval.Pow module, whose strategy computes rigorous interval bounds for x^y via the identity x^y = exp(y · log x) for x > 0. The golden ratio φ is taken from Mathlib as the positive root of t^2 - t - 1 = 0 and serves as the self-similar fixed point throughout Recognition Science. The immediate upstream result is the lemma phi_rpow_mono, whose doc-comment states that φ^x is monotone increasing in x and whose proof reduces to the strict monotonicity of the exponential map.
proof idea
The proof is a one-line wrapper that applies the monotonicity lemma phi_rpow_mono directly to the hypothesis y ≤ z.
why it matters
The result supplies the order-preserving property required for interval propagation of φ-powers inside the Recognition framework. It supports sibling constructions such as phi_pow_neg5_interval and phi_pow_neg3_interval that verify the RS-native values ħ = φ^{-5} and the dream fraction φ^{-3}. The lemma therefore closes a small but necessary step between the abstract monotonicity of the exponential and the concrete phi-ladder bounds used for mass formulas and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.