phi_pow8_in_interval_proven
plain-language theorem explainer
The theorem confirms that the eighth power of the golden ratio lies inside the closed interval [46.97, 46.99]. Numerics researchers anchoring higher powers on the phi-ladder in Recognition Science would cite this containment result. The proof is a short tactic script that splits the contains predicate and invokes the companion strict inequalities phi_pow8_gt and phi_pow8_lt together with norm_num rewrites on the rational endpoints.
Claim. Let $I$ be the closed interval with rational endpoints $4697/100$ and $4699/100$. Then $I$ contains $((1 + sqrt(5))/2)^8$.
background
The module supplies rigorous algebraic bounds on the golden ratio phi = (1 + sqrt(5))/2. It defines Interval as a structure with rational lo and hi endpoints satisfying lo <= hi. The contains predicate on an Interval I and real x holds precisely when (I.lo : R) <= x and x <= (I.hi : R). Upstream lemmas phi_pow8_gt and phi_pow8_lt establish the strict inequalities 46.97 < phi^8 and phi^8 < 46.99 that are reused here. The module's strategy begins with rational bounds on sqrt(5) to derive successive decimal tightenings of phi itself before lifting to integer powers.
proof idea
The tactic proof first simplifies the contains predicate against the concrete interval definition. Constructor splits the resulting conjunction. The lower-bound subgoal invokes phi_pow8_gt and rewrites 4697/100 to 46.97 inside a calc block terminated by norm_num. The upper-bound subgoal applies phi_pow8_lt symmetrically and rewrites 46.99 back to 4699/100.
why it matters
This certified containment supplies a concrete numerical anchor for phi^8 that is consumed by the downstream theorem phi_pow_8_in_interval in the Pow module. It supports the Recognition framework's treatment of phi as the self-similar fixed point by furnishing bounds compatible with the phi-ladder construction. The result closes a small numerical gap without touching open questions on non-integer exponents or physical-constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.