phi_pow_16_in_interval
plain-language theorem explainer
The theorem verifies that the golden ratio raised to the 16th power lies inside the closed rational interval from 2206.9 to 2207.5. Researchers constructing chained interval bounds for higher phi powers in numerical checks of Recognition Science constants would cite this result. The proof unfolds the containment predicate, rewrites the base via the golden ratio formula, reduces the real exponent to a natural number, and splits into lower and upper bounds using two pre-established comparison lemmas.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $2206.9 leq phi^{16} leq 2207.5$.
background
This declaration belongs to the module supplying interval arithmetic for the power function, which obtains rigorous bounds for positive-base powers either via the exp-log identity or by direct evaluation when the exponent is a natural number. An Interval is a structure consisting of rational endpoints lo and hi with lo leq hi; the contains predicate asserts that a real number x satisfies lo leq x leq hi. The local setting follows the module strategy of preferring direct computation for integer exponents to retain higher precision than the general exp-log route.
proof idea
The tactic proof begins by simplifying the contains predicate to expose the concrete interval bounds. It rewrites the base using the identity equating the golden ratio to (1 + sqrt(5))/2, then converts the real exponent 16 into a natural number via rpow_natCast. The goal splits into two inequalities; the lower bound is discharged by applying the pre-proven phi_pow16_gt lemma together with a norm_num calculation, while the upper bound is discharged by applying phi_pow16_lt in the same manner.
why it matters
The result supplies a verified rung on the phi power ladder that is invoked directly by the proof of phi_pow_140_in_interval in the GalacticBounds module. It thereby supports the numerical scaffolding required for Recognition Science derivations that rely on precise phi-ladder intervals, including those appearing in the mass formula and constant evaluations. The bound closes one concrete step in the interval-arithmetic chain needed to connect the self-similar fixed point phi to higher-order numerical claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.