phi_rpow_neg_lt_of_lt
plain-language theorem explainer
The lemma shows that for real y < z the golden ratio to the power -z is strictly smaller than the golden ratio to the power -y. Numerics code that builds interval enclosures for negative phi exponents in the Recognition Science phi-ladder cites this monotonicity fact. The proof is a one-line term that feeds the negated inequality into the already-established strict increase of phi to a real power.
Claim. If $y < z$ for real numbers $y,z$, then $goldenRatio^{-z} < goldenRatio^{-y}$.
background
The Numerics.Interval.Pow module supplies interval arithmetic for the power function on positive reals, relying on the identity $x^y = exp(y log x)$ together with monotonicity of log and exp. For the golden ratio the module maintains dedicated lemmas that track how the exponent interval maps under the power map. The immediate predecessor is the lemma phi_rpow_strictMono, whose doc-comment states that phi > 1 implies phi^x is strictly increasing in x; that fact is proved by invoking Real.rpow_lt_rpow_of_exponent_lt on the base goldenRatio.
proof idea
The proof is a direct term-mode application of phi_rpow_strictMono to the negated hypothesis (neg_lt_neg hyz). Negation reverses the order of y and z, so the known strict increase of the map x |-> goldenRatio^x immediately yields the reversed inequality for the negative exponents.
why it matters
The result supplies the missing negative-exponent half of the monotonicity toolkit required by the interval constructions phi_pow_neg5_interval and phi_pow_neg3_interval that appear among the module siblings. Those intervals in turn feed the phi-ladder mass formulas that rest on the Recognition Science fixed point phi (T6) and the eight-tick octave structure. No downstream theorem is yet recorded as using this lemma, indicating it is still scaffolding the numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.