phi_pow_8_in_interval
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute a decimal expansion of phi^8 beyond the given rational bounds.
- Does not extend the containment claim to non-integer real exponents.
- Does not assert that the supplied interval is the narrowest possible.
- Does not address bases outside the positive reals.
formal statement (Lean)
147theorem phi_pow_8_in_interval : phi_pow_8_interval.contains (((1 + Real.sqrt 5) / 2) ^ (8 : ℝ)) := by
proof body
Tactic-mode proof.
148 simp only [Interval.contains, phi_pow_8_interval]
149 rw [← phi_eq_formula]
150 have h : goldenRatio ^ (8 : ℝ) = goldenRatio ^ 8 := by
151 have : (8 : ℝ) = (8 : ℕ) := by norm_num
152 rw [this, Real.rpow_natCast]
153 rw [h]
154 have hcontains := phi_pow8_in_interval_proven
155 simp only [Interval.contains, phi_pow8_interval_proven] at hcontains
156 exact hcontains
157
158/-- φ^5 interval ≈ 11.09 - PROVEN -/