phi_rpow_interval_bounds
plain-language theorem explainer
The lemma states that powers of the golden ratio preserve order: if the exponent lies between lo and hi then the powered values lie between the powered endpoints. Numerics code in Recognition Science uses it to propagate interval enclosures through expressions involving φ raised to real powers. The proof is a direct term-mode application of the monotonicity lemma to each endpoint inequality separately.
Claim. If $lo ≤ x ≤ hi$ then $φ^{lo} ≤ φ^x ≤ φ^{hi}$, where $φ$ is the golden ratio.
background
The module supplies interval arithmetic for the real power function, relying on the identity $x^y = exp(y log x)$ for positive bases together with monotonicity of log and exp. For the special base $φ > 1$ the module reduces the general strategy to a direct monotonicity argument. The upstream lemma phi_rpow_mono records that the map $x ↦ φ^x$ is monotone increasing on the reals.
proof idea
The proof is a one-line term-mode wrapper. It applies the constructor tactic and invokes phi_rpow_mono once on the lower-bound hypothesis and once on the upper-bound hypothesis.
why it matters
The result supplies the basic interval-propagation rule for φ-powers inside Numerics.Interval.Pow. It supports sibling lemmas that enclose the specific powers $φ^{-5}$, $φ^{-3}$ and $φ^8$ required by the Recognition Science mass formula and Berry creation threshold. The declaration therefore closes a routine but necessary step in the T5–T6 forcing chain that fixes φ as the self-similar constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.