phi_rpow_mono
plain-language theorem explainer
The lemma shows that the real map x to φ raised to x is monotone non-decreasing. Interval-arithmetic code that propagates bounds on powers of the golden ratio cites it whenever an exponent interval is supplied. The proof is a one-line wrapper that extracts the monotone property from the companion strict-monotonicity result.
Claim. The function $f(x) = φ^x$ is monotone increasing on $ℝ$, i.e., $x ≤ y$ implies $φ^x ≤ φ^y$.
background
The module supplies interval arithmetic for the power function by reducing $x^y$ to $exp(y · log x)$ for positive bases. The golden ratio φ > 1 is the self-similar fixed point forced by the Recognition Science chain. The upstream strict-monotonicity lemma establishes φ^y < φ^z whenever y < z by invoking the standard real-analysis fact that a base strictly larger than one yields a strictly increasing exponential.
proof idea
The proof is a one-line wrapper that applies the monotone projection to the companion strict-monotonicity lemma for φ^x.
why it matters
It supplies the monotonicity engine for the three downstream lemmas that deliver interval bounds on φ^x, the order-preserving property φ^y ≤ φ^z for y ≤ z, and the antitone property for negative exponents. These close numeric certification steps for the phi-ladder masses and the alpha band inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.