phi_rpow_lt_of_lt
plain-language theorem explainer
The lemma establishes strict monotonicity of the map x ↦ φ^x for the golden ratio φ > 1. Numerics code constructing interval bounds on φ-powers in Recognition Science would cite it to justify that y < z implies φ^y < φ^z. The proof is a one-line wrapper that invokes the strict monotonicity lemma phi_rpow_strictMono on the given hypothesis.
Claim. Let φ denote the golden ratio. For real numbers y < z, φ^y < φ^z.
background
This lemma belongs to the Numerics.Interval.Pow module, which supplies rigorous interval arithmetic for the power function via the identity x^y = exp(y · log x) when x > 0. The module computes enclosures by first bounding the logarithm, scaling by the exponent interval, and applying the exponential map, with special handling for natural-number exponents via direct computation.
proof idea
The proof is a one-line wrapper that applies phi_rpow_strictMono to the hypothesis y < z. The upstream lemma phi_rpow_strictMono itself reduces to the Mathlib fact Real.rpow_lt_rpow_of_exponent_lt using the fact that goldenRatio > 1.
why it matters
The result supplies the monotonicity needed to build the sibling interval declarations such as phi_pow_neg5_interval and phi_pow_8_interval. It supports the phi-ladder mass formula and the constants ħ = φ^{-5}, G = φ^5 / π in the Recognition Science framework by ensuring exponent comparisons translate directly into value comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.