phi_pow_neg5_interval
plain-language theorem explainer
The definition supplies a closed rational interval [89/1000, 91/1000] containing φ^{-5}. Numerics code that certifies bounds on golden-ratio powers in Recognition Science cites it to obtain rigorous containment. It is a direct definition that copies the bounds already established for (φ^{-1})^5 and checks the ordering condition by norm_num.
Claim. Define the closed interval $I$ with rational endpoints $lo = 89/1000$ and $hi = 91/1000$ satisfying $lo ≤ hi$. This interval contains the value φ^{-5} where φ = (1 + √5)/2.
background
The Interval structure is a closed interval with rational endpoints lo and hi where lo ≤ hi. The upstream phi_inv5_interval_proven supplies an identical interval containing (φ^{-1})^5, established by direct norm_num. The module develops interval arithmetic for the power function via x^y = exp(y log x) for x > 0, with direct computation reserved for integer powers of φ to maintain precision.
proof idea
This is a one-line wrapper definition that reuses the bounds from phi_inv5_interval_proven for the lower and upper endpoints and discharges the validity obligation with the norm_num tactic.
why it matters
This interval is used by the theorem phi_pow_neg5_in_interval to prove that ((1 + √5)/2)^{-5} lies inside the interval. It supports the Recognition framework by supplying certified bounds on φ powers that enter the mass formula on the phi-ladder and the self-similar fixed point at T6. The construction closes a numerics gap that helps verify the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.