phi_pow_5_in_interval
This theorem places the fifth power of the golden ratio inside the rational interval from 11.09 to 11.1. Researchers verifying numerical bounds on iterated powers of phi for Recognition Science mass ladders or galactic scaling would cite the result. The proof rewrites the expression via the closed-form definition of phi, reduces the exponent to a natural number, then splits the containment goal into two inequalities supplied by prior bounds on phi^5.
claimLet $I = [11.09, 11.1]$ be the closed interval with rational endpoints. Then $I$ contains the real number $((1 + sqrt(5))/2)^5$.
background
The module supplies interval arithmetic for the power function, using the identity x^y = exp(y log x) for positive x and direct computation for natural-number exponents. An Interval is a structure with rational lo and hi endpoints satisfying lo <= hi. The predicate contains(I, x) holds precisely when lo <= x <= hi. The golden ratio is identified with the Mathlib constant goldenRatio via the theorem that equates it to (1 + sqrt(5))/2. Two upstream results supply the strict inequalities 11.09 < goldenRatio^5 and goldenRatio^5 < 11.1, each proved by rewriting to an algebraic expression in phi and applying linear arithmetic.
proof idea
The tactic proof first simplifies the containment predicate, rewrites the base via the closed-form identity for the golden ratio, and normalizes the exponent from real 5 to natural 5 using rpow_natCast. It then splits the resulting conjunction and discharges each side by a calculation that invokes the pre-proved strict bounds phi_pow5_gt and phi_pow5_lt, converting the rational constants via norm_num.
why it matters in Recognition Science
The result supplies the base case for composing higher powers of phi inside interval arithmetic, directly feeding the proofs that phi^140 and phi^145 lie inside their respective intervals in the GalacticBounds module. It therefore supports the numerical verification of the phi-ladder mass formula and the eight-tick octave scaling that Recognition Science derives from the J-uniqueness fixed point. No open scaffolding remains for this specific bound.
scope and limits
- Does not compute the exact decimal expansion of phi^5 beyond the given interval.
- Does not address non-integer or negative exponents for the same base.
- Does not generalize the interval construction to arbitrary real bases.
- Does not replace the need for separate proofs of the bounding inequalities themselves.
Lean usage
have h5 : phi_pow_5_interval.contains (goldenRatio ^ (5 : ℝ)) := phi_pow_5_in_intervalformal statement (Lean)
164theorem phi_pow_5_in_interval : phi_pow_5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (5 : ℝ)) := by
proof body
Tactic-mode proof.
165 simp only [Interval.contains, phi_pow_5_interval]
166 rw [← phi_eq_formula]
167 have h : goldenRatio ^ (5 : ℝ) = goldenRatio ^ 5 := by
168 have : (5 : ℝ) = (5 : ℕ) := by norm_num
169 rw [this, Real.rpow_natCast]
170 rw [h]
171 constructor
172 · have h1 := phi_pow5_gt
173 calc ((1109 / 100 : ℚ) : ℝ) = (11.09 : ℝ) := by norm_num
174 _ ≤ goldenRatio ^ 5 := le_of_lt h1
175 · have h1 := phi_pow5_lt
176 calc goldenRatio ^ 5 ≤ (11.1 : ℝ) := le_of_lt h1
177 _ = ((111 / 10 : ℚ) : ℝ) := by norm_num
178
179/-- φ^16 interval ≈ 2207 - PROVEN -/