phi_pow_neg5_interval
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not compute the exact value of φ^{-5}.
- Does not provide bounds for arbitrary real exponents.
- Does not incorporate physical measurement uncertainty.
- Does not invoke the Recognition Composition Law.
formal statement (Lean)
75def phi_pow_neg5_interval : Interval where
76 lo := 89 / 1000 -- Matches phi_inv5_interval_proven
proof body
Definition body.
77 hi := 91 / 1000
78 valid := by norm_num
79