phi_pow_5_interval
plain-language theorem explainer
The definition supplies the closed rational interval [11.09, 11.1] that contains the fifth power of the golden ratio. Numerics code in the Recognition Science project cites it when composing bounds for higher powers such as φ^140 and φ^145 used in galactic-ratio comparisons. The declaration is realized directly by setting the endpoints and discharging the ordering obligation with norm_num.
Claim. The closed interval $[1109/100, 111/10]$ contains $φ^5$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module implements interval arithmetic for real powers via the identity $x^y = exp(y · log x)$ for $x > 0$, with a special direct path for natural-number exponents. An Interval is a structure carrying rational endpoints lo and hi together with a proof that lo ≤ hi. This definition provides a concrete enclosure for φ^5 that is later multiplied with other power intervals inside GalacticBounds.
proof idea
The declaration is a direct definition that records lo := 1109/100, hi := 111/10 and invokes the norm_num tactic to confirm the validity field.
why it matters
The interval serves as a reusable building block for the power-composition lemmas in GalacticBounds, including phi_pow_145_interval (which multiplies it by phi_pow_140_interval) and the comparison theorems phi_pow_140_lt_ratio and phi_pow_142_lt_ratio_1_3. It supports the Recognition Science program of obtaining rigorous enclosures for powers of φ that appear on the phi-ladder and in the eight-tick octave. Downstream results quote the interval explicitly when unfolding higher-power definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.