rpowIntervalSimple_contains_rpow
plain-language theorem explainer
The theorem states that if rational bounds a ≤ b enclose the real value x^y, then the interval built from those bounds contains x^y. Numerics routines that enclose exponentiation in the Recognition framework cite this to justify direct bound packaging. The proof is a one-line term that constructs the containment predicate directly from the two supplied inequalities.
Claim. Let $a, b$ be rationals with $a ≤ b$. If $a ≤ x^y ≤ b$ for reals $x, y$, then $x^y$ belongs to the closed interval with rational endpoints $a$ and $b$.
background
The module supplies interval arithmetic for the power function via the identity x^y = exp(y log x) for x > 0, with a simple constructor for cases where explicit bounds on the result are already known. An Interval is a structure with rational lo and hi endpoints together with a proof that lo ≤ hi. The predicate contains holds for a real z precisely when lo ≤ z ≤ hi. The auxiliary definition rpowIntervalSimple simply packages given rational bounds into such an Interval.
proof idea
The proof is a one-line term that applies the definition of contains by returning the pair of the two supplied inequalities.
why it matters
This containment result is the base case for power-interval construction in the numerics layer. It supports sibling lemmas that bound specific powers of the golden ratio (phi^(-5), phi^(-3), phi^51, etc.) used to realize constants such as ħ = phi^(-5) and the alpha band. The declaration closes the explicit-bound case before more involved log-exp interval arithmetic is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.