phi_pow_neg5_in_interval
plain-language theorem explainer
The theorem establishes that ((1 + √5)/2)^{-5} lies inside the rational interval [0.089, 0.091]. Recognition Science numerics code cites it to bound ħ = φ^{-5} in native units without floating-point error. The proof reduces the claim via the identity φ^{-5} = (φ^{-1})^5 to the already-proven containment of (φ^{-1})^5, then verifies the endpoints by direct linarith comparison.
Claim. Let $φ = (1 + √5)/2$. Then $φ^{-5} ∈ [89/1000, 91/1000]$.
background
The module supplies interval arithmetic for the power function via the identity x^y = exp(y · log x) for x > 0, with a special direct path for integer powers of φ. An Interval is a closed rational interval [lo, hi] with lo ≤ hi; the contains predicate holds when lo ≤ x ≤ hi. The upstream phi_inv5_interval_proven defines the interval [89/1000, 91/1000] and proves it contains (φ^{-1})^5. phi_eq_formula identifies Mathlib's goldenRatio with the closed-form expression for φ.
proof idea
The tactic proof rewrites the target using phi_eq_formula, establishes the identity goldenRatio^{-5} = (goldenRatio^{-1})^5 via Real.rpow_neg and inv_pow, obtains the containment from phi_inv5_in_interval_proven, normalizes the rational endpoints 89/1000 and 91/1000, and closes the two inequalities by linarith.
why it matters
This theorem supplies a machine-checked bound on φ^{-5} that supports the Recognition Science constants ħ = φ^{-5} and the phi-ladder mass formula. It closes one link in the numerics required for the eight-tick octave and D = 3 derivations. No downstream uses are recorded yet, but the result is a prerequisite for certified computation of the fine-structure constant interval (137.030, 137.039) or particle masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.