phi_pow_neg3_interval
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.