phi_pow_neg3_interval
The definition supplies the closed rational interval [2359/10000, 237/1000] asserted to contain φ^{-3}. Numerics code certifying golden-ratio powers in the Recognition framework cites this interval to avoid floating-point error. Construction is a direct endpoint assignment with norm_num discharging the lo ≤ hi check.
claimLet $I = [2359/10000, 237/1000]$ be the closed interval with rational endpoints satisfying $2359/10000 ≤ 237/1000$. This interval is constructed to contain $φ^{-3}$ where $φ = (1 + √5)/2$.
background
The Interval structure is a closed interval with rational endpoints lo and hi satisfying lo ≤ hi. The module supplies interval arithmetic for the power function via the identity x^y = exp(y log x), with direct computation used for integer exponents on φ. This definition reuses the endpoints from the proven interval containing (φ^{-1})^3.
proof idea
Direct definition that assigns the lower and upper bounds to match the proven φ^{-3} interval and applies norm_num to the validity predicate.
why it matters in Recognition Science
The interval is used by the theorem that certifies ((1 + √5)/2)^{-3} lies inside it. It supports numerical certification of φ powers that appear in the phi-ladder and mass formulas of the Recognition framework. The bounds are consistent with the self-similar fixed point φ from the forcing chain.
scope and limits
- Does not establish that the real value φ^{-3} lies inside the interval.
- Does not compute bounds for arbitrary bases or exponents.
- Does not invoke interval arithmetic operations on logs or exponentials.
- Does not depend on any floating-point representation.
formal statement (Lean)
99def phi_pow_neg3_interval : Interval where
100 lo := 2359 / 10000 -- Matches phi_inv3_interval_proven
proof body
Definition body.
101 hi := 237 / 1000
102 valid := by norm_num
103