phi_inv_lt
The declaration establishes the strict inequality φ^{-1} < 0.6186 for the golden ratio reciprocal. Numerics specialists in Recognition Science cite it to control error terms when enclosing powers of φ^{-1} inside intervals. The proof reduces the claim via the algebraic identity φ^{-1} = φ - 1 and closes it with the companion bound φ < 1.6185 using linear arithmetic.
claim$φ^{-1} < 0.6186$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module Numerics.Interval.PhiBounds develops rigorous decimal bounds on the golden ratio φ by starting from rational approximations to √5. The Interval structure provides a closed interval with rational endpoints lo ≤ hi. Upstream results include the identity theorem phi_inv_eq asserting φ^{-1} = φ - 1, and the bound phi_lt_16185 that φ < 1.6185 obtained from √5 < 2.237.
proof idea
The term-mode proof rewrites the left side using phi_inv_eq to obtain φ - 1 < 0.6186. It then applies the hypothesis from phi_lt_16185 that φ < 1.6185 and finishes with linarith.
why it matters in Recognition Science
This result supplies the base case for the chain of bounds on negative powers of φ that appear in phi_inv2_lt and phi_inv3_lt. It also supports the interval membership proof phi_inv_in_interval_proven. Within the framework it anchors the numerical side of the phi-ladder by confirming concrete upper bounds consistent with the self-similar fixed point property of φ.
scope and limits
- Does not prove a matching lower bound on φ^{-1}.
- Does not apply the bound outside real numbers.
- Does not derive the constant 0.6186 from first principles.
- Does not address convergence rates for iterated powers.
formal statement (Lean)
267theorem phi_inv_lt : goldenRatio⁻¹ < (0.6186 : ℝ) := by
proof body
Term-mode proof.
268 rw [phi_inv_eq]
269 have h := phi_lt_16185
270 linarith
271
272/-- Interval containing φ⁻¹ - PROVEN -/