phi_pow_8_in_interval
plain-language theorem explainer
The theorem confirms that ((1 + sqrt(5))/2)^8 lies inside the closed rational interval with bounds 46.97 and 46.99. Numerics researchers verifying phi-ladder bounds cite it to certify the eighth power without floating-point issues. The tactic proof rewrites the base via the golden-ratio identity, converts the exponent to a natural number, and delegates containment to a pre-proven interval theorem.
Claim. Let $I$ be the closed interval with rational endpoints $4697/100$ and $4699/100$. Then $((1 + sqrt(5))/2)^8$ belongs to $I$.
background
The Interval structure is a closed interval with rational endpoints lo and hi satisfying lo ≤ hi. Its contains predicate holds for a real x precisely when lo ≤ x ≤ hi. The module supplies interval arithmetic for the power function via the identity x^y = exp(y log x) for x > 0, with a direct route for natural-number exponents that avoids log-exp rounding. The upstream phi_pow8_interval_proven definition fixes the concrete bounds [4697/100, 4699/100] and its companion theorem already establishes containment of goldenRatio^8 inside those bounds. The sibling phi_eq_formula records the identity goldenRatio = (1 + sqrt(5))/2.
proof idea
The tactic proof first unfolds contains on the target interval, rewrites the base via phi_eq_formula to reach goldenRatio, converts the real exponent 8 to a natural number with norm_num and rpow_natCast, then applies the already-proven containment phi_pow8_in_interval_proven after unfolding its own contains predicate.
why it matters
This result supplies a machine-checked anchor for phi^8 inside the numerics module, supporting the phi-ladder mass formulas and the eight-tick octave step (T7) of the forcing chain. It closes the verification for the concrete power that appears in the phi^8 interval used by higher Recognition numerics. No downstream declarations are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.